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

Theorem unipw 5316
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 𝒫 𝐴 = 𝐴

Proof of Theorem unipw
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 4814 . . . 4 (𝑥 𝒫 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦 ∈ 𝒫 𝐴))
2 elelpwi 4524 . . . . 5 ((𝑥𝑦𝑦 ∈ 𝒫 𝐴) → 𝑥𝐴)
32exlimiv 1932 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ 𝒫 𝐴) → 𝑥𝐴)
41, 3sylbi 220 . . 3 (𝑥 𝒫 𝐴𝑥𝐴)
5 vsnid 4575 . . . 4 𝑥 ∈ {𝑥}
6 snelpwi 5310 . . . 4 (𝑥𝐴 → {𝑥} ∈ 𝒫 𝐴)
7 elunii 4816 . . . 4 ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 𝒫 𝐴)
85, 6, 7sylancr 590 . . 3 (𝑥𝐴𝑥 𝒫 𝐴)
94, 8impbii 212 . 2 (𝑥 𝒫 𝐴𝑥𝐴)
109eqriv 2818 1 𝒫 𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1538  wex 1781  wcel 2115  𝒫 cpw 4512  {csn 4540   cuni 4811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-pw 4514  df-sn 4541  df-pr 4543  df-uni 4812
This theorem is referenced by:  univ  5317  pwtr  5318  unixpss  5656  pwexr  7462  unifpw  8803  fiuni  8868  ween  9438  fin23lem41  9751  mremre  16853  submre  16854  isacs1i  16906  eltg4i  21543  distop  21578  distopon  21580  distps  21598  ntrss2  21640  isopn3  21649  discld  21672  mretopd  21675  dishaus  21965  discmp  21981  dissnlocfin  22112  locfindis  22113  txdis  22215  xkopt  22238  xkofvcn  22267  hmphdis  22379  ustbas2  22809  vitali  24195  shsupcl  29099  shsupunss  29107  iundifdifd  30299  iundifdif  30300  dispcmp  31133  mbfmcnt  31533  omssubadd  31565  carsgval  31568  carsggect  31583  coinflipprob  31744  coinflipuniv  31746  fnemeet2  33722  bj-unirel  34360  bj-discrmoore  34419  icoreunrn  34656  ctbssinf  34703  mapdunirnN  38824  ismrcd1  39434  hbt  39869  pwelg  40054  pwsal  42748  salgenval  42754  salgenn0  42762  salexct  42765  salgencntex  42774  0ome  42959  isomennd  42961  unidmovn  43043  rrnmbl  43044  hspmbl  43059
  Copyright terms: Public domain W3C validator