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

Theorem unipw 4224
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 3830 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3635 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 1666 . . . 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 2791 . . . . 5  |-  x  e. 
_V
65snid 3667 . . . 4  |-  x  e. 
{ x }
7 snelpwi 4220 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
8 elunii 3832 . . . 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 2280 1  |-  U. ~P A  =  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   ~Pcpw 3625   {csn 3640   U.cuni 3827
This theorem is referenced by:  pwtr  4226  pwexb  4564  univ  4565  unixpss  4799  unifpw  7158  fiuni  7181  ween  7662  fin23lem41  7978  mremre  13506  submre  13507  isacs1i  13559  eltg4i  16698  distop  16733  distopon  16734  distps  16752  ntrss2  16794  isopn3  16803  discld  16826  mretopd  16829  dishaus  17110  discmp  17125  txdis  17326  xkopt  17349  xkofvcn  17378  hmphdis  17487  vitali  18968  shsupcl  21917  shsupunss  21925  iundifdifd  23159  iundifdif  23160  mbfmcnt  23573  coinflipprob  23680  coinflipuniv  23682  usptoplem  25546  istopx  25547  usptop  25550  tartarmap  25888  locfindis  26305  fnemeet2  26316  ismrcd1  26773  hbt  27334  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-pw 3627  df-sn 3646  df-pr 3647  df-uni 3828
  Copyright terms: Public domain W3C validator