Theorem unipw 3504

Description: A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (The proof was shortened by Alan Sare, 28-Dec-2008.)

Assertion

Ref	Expression
unipw	|- U.~PA = A

Proof of Theorem unipw

Step	Hyp	Ref	Expression
1		eluni 3180	. . . 4 |- (x e. U.~PA <-> E.y(x e. y /\ y e. ~PA))
2		visset 2295	. . . . . . . 8 |- y e. _V
3	2	elpw 3037	. . . . . . 7 |- (y e. ~PA <-> y C_ A)
4		ssel 2615	. . . . . . 7 |- (y C_ A -> (x e. y -> x e. A))
5	3, 4	sylbi 216	. . . . . 6 |- (y e. ~PA -> (x e. y -> x e. A))
6	5	impcom 378	. . . . 5 |- ((x e. y /\ y e. ~PA) -> x e. A)
7	6	19.23aiv 1674	. . . 4 |- (E.y(x e. y /\ y e. ~PA) -> x e. A)
8	1, 7	sylbi 216	. . 3 |- (x e. U.~PA -> x e. A)
9		elunii 3182	. . . 4 |- ((x e. {x} /\ {x} e. ~PA) -> x e. U.~PA)
10		visset 2295	. . . . 5 |- x e. _V
11	10	snid 3069	. . . 4 |- x e. {x}
12	10	snelpw 3501	. . . . 5 |- (x e. A <-> {x} e. ~PA)
13	12	biimpi 168	. . . 4 |- (x e. A -> {x} e. ~PA)
14	9, 11, 13	sylancr 526	. . 3 |- (x e. A -> x e. U.~PA)
15	8, 14	impbii 174	. 2 |- (x e. U.~PA <-> x e. A)
16	15	eqriv 1881	1 |- U.~PA = A

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326   C_ wss 2593  ~Pcpw 3032  {csn 3044  U.cuni 3177

This theorem is referenced by:  pwexb 3852  univ 3853  unixpss 4094  unirnioo 7571  distop 8919  distps 8924  cncnplem1 9051  uniopn2 9138  opnuni 9145  dfchsup2 10931  hsupval2 10933  hsupval 10934  shsupcl 10939  shsupunss 10948  mapdiscnlem 14870  usptoplem 14917  istopx 14918  prtoptop 14919  usptop 14920  fgsb 14921  dtopcl 14948  dtt2 14951  tartarmap 15265  locfindsc 15515  topmtcl 15525  totbndss 15937  heiborlem23 15977

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-uni 3178

Copyright terms: Public domain