Theorem class2set 2702

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 2692	. 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 1706	. . . 4 |- (-. A e. V -> -. E.x e. A A e. V)
4		rabn0 2263	. . . . 5 |- ({x e. A | A e. V} =/= (/) <-> E.x e. A A e. V)
5	4	necon1bbii 1593	. . . 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 2679	. . 3 |- (/) e. V
8	6, 7	syl6eqel 1532	. 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 1099   e. wcel 1105  E.wrex 1622  {crab 1624  Vcvv 1786  (/)c0 2251

This theorem is referenced by:  abrexex 3799  fsum1s 6898  fsump1s 6902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-rab 1628  df-v 1787  df-dif 2020  df-in 2022  df-ss 2024  df-nul 2252

Copyright terms: Public domain