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

Theorem unipw 4118
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 3730 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3539 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 2023 . . . 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 2730 . . . . 5  |-  x  e. 
_V
65snid 3571 . . . 4  |-  x  e. 
{ x }
7 snelpwi 4114 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
8 elunii 3732 . . . 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 2250 1  |-  U. ~P A  =  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1537    = wceq 1619    e. wcel 1621   ~Pcpw 3530   {csn 3544   U.cuni 3727
This theorem is referenced by:  pwtr  4120  pwexb  4455  univ  4456  unixpss  4706  unifpw  7042  fiuni  7065  ween  7546  fin23lem41  7862  mremre  13378  submre  13379  isacs1i  13403  eltg4i  16530  distop  16565  distopon  16566  distps  16584  ntrss2  16626  isopn3  16635  discld  16658  mretopd  16661  dishaus  16942  discmp  16957  txdis  17158  xkopt  17181  xkofvcn  17210  hmphdis  17319  vitali  18800  shsupcl  21747  shsupunss  21755  usptoplem  24712  istopx  24713  usptop  24716  tartarmap  25054  locfindis  25471  fnemeet2  25482  ismrcd1  25939  hbt  26500  mapdunirnN  30529
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-pw 3532  df-sn 3550  df-pr 3551  df-uni 3728
  Copyright terms: Public domain W3C validator