Theorem class2set 2734

Description: Construct, from any class A, a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists.

Assertion

Ref	Expression
class2set	|- {x e. A | A e. V} e. V

Distinct variable group:   x,A

Proof of Theorem class2set

Step	Hyp	Ref	Expression
1		rabexg 2724	. 2 |- (A e. V -> {x e. A | A e. V} e. V)
2		pm3.26 319	. . . . 5 |- ((-. A e. V /\ x e. A) -> -. A e. V)
3	2	nrexdv 1730	. . . 4 |- (-. A e. V -> -. E.x e. A A e. V)
4		rabn0 2292	. . . . 5 |- ({x e. A | A e. V} =/= (/) <-> E.x e. A A e. V)
5	4	necon1bbii 1617	. . . 4 |- (-. E.x e. A A e. V <-> {x e. A | A e. V} = (/))
6	3, 5	sylib 198	. . 3 |- (-. A e. V -> {x e. A | A e. V} = (/))
7		0ex 2711	. . 3 |- (/) e. V
8	6, 7	syl6eqel 1556	. 2 |- (-. A e. V -> {x e. A | A e. V} e. V)
9	1, 8	pm2.61i 126	1 |- {x e. A | A e. V} e. V

Syntax hints:  -. wn 2   = wceq 956   e. wcel 958  E.wrex 1646  {crab 1648  Vcvv 1811  (/)c0 2280

This theorem is referenced by:  abrexex 3860  fsum1s 7009  fsump1s 7013

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-nul 2710

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-rab 1652  df-v 1812  df-dif 2049  df-in 2051  df-ss 2053  df-nul 2281

Copyright terms: Public domain