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

Theorem unipw 4374
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 3978 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3769 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 1641 . . . 4  |-  ( E. y ( x  e.  y  /\  y  e. 
~P A )  ->  x  e.  A )
41, 3sylbi 188 . . 3  |-  ( x  e.  U. ~P A  ->  x  e.  A )
5 vex 2919 . . . . 5  |-  x  e. 
_V
65snid 3801 . . . 4  |-  x  e. 
{ x }
7 snelpwi 4369 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
8 elunii 3980 . . . 4  |-  ( ( x  e.  { x }  /\  { x }  e.  ~P A )  ->  x  e.  U. ~P A
)
96, 7, 8sylancr 645 . . 3  |-  ( x  e.  A  ->  x  e.  U. ~P A )
104, 9impbii 181 . 2  |-  ( x  e.  U. ~P A  <->  x  e.  A )
1110eqriv 2401 1  |-  U. ~P A  =  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721   ~Pcpw 3759   {csn 3774   U.cuni 3975
This theorem is referenced by:  pwtr  4376  pwexb  4712  univ  4713  unixpss  4947  unifpw  7367  fiuni  7391  ween  7872  fin23lem41  8188  mremre  13784  submre  13785  isacs1i  13837  eltg4i  16980  distop  17015  distopon  17016  distps  17034  ntrss2  17076  isopn3  17085  discld  17108  mretopd  17111  dishaus  17400  discmp  17415  txdis  17617  xkopt  17640  xkofvcn  17669  hmphdis  17781  ustbas2  18208  vitali  19458  shsupcl  22793  shsupunss  22801  iundifdifd  23965  iundifdif  23966  mbfmcnt  24571  coinflipprob  24690  coinflipuniv  24692  locfindis  26275  fnemeet2  26286  ismrcd1  26642  hbt  27202  mapdunirnN  32133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-pw 3761  df-sn 3780  df-pr 3781  df-uni 3976
  Copyright terms: Public domain W3C validator