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

Theorem unipw 4697
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 4248 . . . 4  |-  ( x  e.  U. ~P A  <->  E. y ( x  e.  y  /\  y  e. 
~P A ) )
2 elelpwi 4021 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ~P A
)  ->  x  e.  A )
32exlimiv 1698 . . . 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 4056 . . . 4  |-  x  e. 
{ x }
6 snelpwi 4692 . . . 4  |-  ( x  e.  A  ->  { x }  e.  ~P A
)
7 elunii 4250 . . . 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 2463 1  |-  U. ~P A  =  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767   ~Pcpw 4010   {csn 4027   U.cuni 4245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-pw 4012  df-sn 4028  df-pr 4030  df-uni 4246
This theorem is referenced by:  univ  4698  pwtr  4700  unixpss  5118  pwexb  6595  unifpw  7823  fiuni  7888  ween  8416  fin23lem41  8732  mremre  14859  submre  14860  isacs1i  14912  eltg4i  19256  distop  19291  distopon  19292  distps  19310  ntrss2  19352  isopn3  19361  discld  19384  mretopd  19387  dishaus  19677  discmp  19692  txdis  19896  xkopt  19919  xkofvcn  19948  hmphdis  20060  ustbas2  20491  vitali  21785  shsupcl  25960  shsupunss  25968  iundifdifd  27130  iundifdif  27131  mbfmcnt  27907  omsfval  27933  oms0  27934  omsmon  27935  coinflipprob  28086  coinflipuniv  28088  locfindis  29805  fnemeet2  29816  ismrcd1  30262  hbt  30711  mapdunirnN  36465
  Copyright terms: Public domain W3C validator