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

Theorem unipw 4240
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 3846 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3648 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 1624 . . . 4  |-  ( E. y ( x  e.  y  /\  y  e. 
~P A )  ->  x  e.  A )
41, 3sylbi 187 . . 3  |-  ( x  e.  U. ~P A  ->  x  e.  A )
5 vex 2804 . . . . 5  |-  x  e. 
_V
65snid 3680 . . . 4  |-  x  e. 
{ x }
7 snelpwi 4236 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
8 elunii 3848 . . . 4  |-  ( ( x  e.  { x }  /\  { x }  e.  ~P A )  ->  x  e.  U. ~P A
)
96, 7, 8sylancr 644 . . 3  |-  ( x  e.  A  ->  x  e.  U. ~P A )
104, 9impbii 180 . 2  |-  ( x  e.  U. ~P A  <->  x  e.  A )
1110eqriv 2293 1  |-  U. ~P A  =  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1531    = wceq 1632    e. wcel 1696   ~Pcpw 3638   {csn 3653   U.cuni 3843
This theorem is referenced by:  pwtr  4242  pwexb  4580  univ  4581  unixpss  4815  unifpw  7174  fiuni  7197  ween  7678  fin23lem41  7994  mremre  13522  submre  13523  isacs1i  13575  eltg4i  16714  distop  16749  distopon  16750  distps  16768  ntrss2  16810  isopn3  16819  discld  16842  mretopd  16845  dishaus  17126  discmp  17141  txdis  17342  xkopt  17365  xkofvcn  17394  hmphdis  17503  vitali  18984  shsupcl  21933  shsupunss  21941  iundifdifd  23175  iundifdif  23176  mbfmcnt  23588  coinflipprob  23695  coinflipuniv  23697  usptoplem  25649  istopx  25650  usptop  25653  tartarmap  25991  locfindis  26408  fnemeet2  26419  ismrcd1  26876  hbt  27437  mapdunirnN  32462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-pw 3640  df-sn 3659  df-pr 3660  df-uni 3844
  Copyright terms: Public domain W3C validator