MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unipw Unicode version

Theorem unipw 4196
Description: A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.)
Assertion
Ref Expression
unipw  |-  U. ~P A  =  A

Proof of Theorem unipw
StepHypRef Expression
1 eluni 3804 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3609 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 2024 . . . 4  |-  ( E. y ( x  e.  y  /\  y  e. 
~P A )  ->  x  e.  A )
41, 3sylbi 189 . . 3  |-  ( x  e.  U. ~P A  ->  x  e.  A )
5 vex 2766 . . . . 5  |-  x  e. 
_V
65snid 3641 . . . 4  |-  x  e. 
{ x }
7 snelpwi 4192 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
8 elunii 3806 . . . 4  |-  ( ( x  e.  { x }  /\  { x }  e.  ~P A )  ->  x  e.  U. ~P A
)
96, 7, 8sylancr 647 . . 3  |-  ( x  e.  A  ->  x  e.  U. ~P A )
104, 9impbii 182 . 2  |-  ( x  e.  U. ~P A  <->  x  e.  A )
1110eqriv 2255 1  |-  U. ~P A  =  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1537    = wceq 1619    e. wcel 1621   ~Pcpw 3599   {csn 3614   U.cuni 3801
This theorem is referenced by:  pwtr  4198  pwexb  4536  univ  4537  unixpss  4787  unifpw  7126  fiuni  7149  ween  7630  fin23lem41  7946  mremre  13468  submre  13469  isacs1i  13521  eltg4i  16660  distop  16695  distopon  16696  distps  16714  ntrss2  16756  isopn3  16765  discld  16788  mretopd  16791  dishaus  17072  discmp  17087  txdis  17288  xkopt  17311  xkofvcn  17340  hmphdis  17449  vitali  18930  shsupcl  21877  shsupunss  21885  usptoplem  24913  istopx  24914  usptop  24917  tartarmap  25255  locfindis  25672  fnemeet2  25683  ismrcd1  26140  hbt  26701  mapdunirnN  31007
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-pw 3601  df-sn 3620  df-pr 3621  df-uni 3802
  Copyright terms: Public domain W3C validator