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

Theorem unipw 4547
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 4099 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 3876 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 1688 . . . 4  |-  ( E. y ( x  e.  y  /\  y  e. 
~P A )  ->  x  e.  A )
41, 3sylbi 195 . . 3  |-  ( x  e.  U. ~P A  ->  x  e.  A )
5 ssnid 3911 . . . 4  |-  x  e. 
{ x }
6 snelpwi 4542 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
7 elunii 4101 . . . 4  |-  ( ( x  e.  { x }  /\  { x }  e.  ~P A )  ->  x  e.  U. ~P A
)
85, 6, 7sylancr 663 . . 3  |-  ( x  e.  A  ->  x  e.  U. ~P A )
94, 8impbii 188 . 2  |-  ( x  e.  U. ~P A  <->  x  e.  A )
109eqriv 2440 1  |-  U. ~P A  =  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   ~Pcpw 3865   {csn 3882   U.cuni 4096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-pw 3867  df-sn 3883  df-pr 3885  df-uni 4097
This theorem is referenced by:  univ  4548  pwtr  4550  unixpss  4960  pwexb  6392  unifpw  7619  fiuni  7683  ween  8210  fin23lem41  8526  mremre  14547  submre  14548  isacs1i  14600  eltg4i  18570  distop  18605  distopon  18606  distps  18624  ntrss2  18666  isopn3  18675  discld  18698  mretopd  18701  dishaus  18991  discmp  19006  txdis  19210  xkopt  19233  xkofvcn  19262  hmphdis  19374  ustbas2  19805  vitali  21098  shsupcl  24746  shsupunss  24754  iundifdifd  25917  iundifdif  25918  mbfmcnt  26688  omsfval  26714  oms0  26715  omsmon  26716  coinflipprob  26867  coinflipuniv  26869  locfindis  28582  fnemeet2  28593  ismrcd1  29039  hbt  29491  mapdunirnN  35300
  Copyright terms: Public domain W3C validator