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

Theorem unipw 4415
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 4019 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3810 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 1645 . . . 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 2960 . . . . 5  |-  x  e. 
_V
65snid 3842 . . . 4  |-  x  e. 
{ x }
7 snelpwi 4410 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
8 elunii 4021 . . . 4  |-  ( ( x  e.  { x }  /\  { x }  e.  ~P A )  ->  x  e.  U. ~P A
)
96, 7, 8sylancr 646 . . 3  |-  ( x  e.  A  ->  x  e.  U. ~P A )
104, 9impbii 182 . 2  |-  ( x  e.  U. ~P A  <->  x  e.  A )
1110eqriv 2434 1  |-  U. ~P A  =  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   ~Pcpw 3800   {csn 3815   U.cuni 4016
This theorem is referenced by:  pwtr  4417  pwexb  4754  univ  4755  unixpss  4989  unifpw  7410  fiuni  7434  ween  7917  fin23lem41  8233  mremre  13830  submre  13831  isacs1i  13883  eltg4i  17026  distop  17061  distopon  17062  distps  17080  ntrss2  17122  isopn3  17131  discld  17154  mretopd  17157  dishaus  17447  discmp  17462  txdis  17665  xkopt  17688  xkofvcn  17717  hmphdis  17829  ustbas2  18256  vitali  19506  shsupcl  22841  shsupunss  22849  iundifdifd  24013  iundifdif  24014  mbfmcnt  24619  coinflipprob  24738  coinflipuniv  24740  locfindis  26386  fnemeet2  26397  ismrcd1  26753  hbt  27312  mapdunirnN  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pr 4404
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-pw 3802  df-sn 3821  df-pr 3822  df-uni 4017
  Copyright terms: Public domain W3C validator