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

Theorem unipw 4839
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 4369 . . . 4 (𝑥 𝒫 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦 ∈ 𝒫 𝐴))
2 elelpwi 4118 . . . . 5 ((𝑥𝑦𝑦 ∈ 𝒫 𝐴) → 𝑥𝐴)
32exlimiv 1844 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ 𝒫 𝐴) → 𝑥𝐴)
41, 3sylbi 205 . . 3 (𝑥 𝒫 𝐴𝑥𝐴)
5 vsnid 4155 . . . 4 𝑥 ∈ {𝑥}
6 snelpwi 4834 . . . 4 (𝑥𝐴 → {𝑥} ∈ 𝒫 𝐴)
7 elunii 4371 . . . 4 ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 𝒫 𝐴)
85, 6, 7sylancr 693 . . 3 (𝑥𝐴𝑥 𝒫 𝐴)
94, 8impbii 197 . 2 (𝑥 𝒫 𝐴𝑥𝐴)
109eqriv 2606 1 𝒫 𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wex 1694  wcel 1976  𝒫 cpw 4107  {csn 4124   cuni 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-pw 4109  df-sn 4125  df-pr 4127  df-uni 4367
This theorem is referenced by:  univ  4840  pwtr  4842  unixpss  5146  pwexb  6844  unifpw  8129  fiuni  8194  ween  8718  fin23lem41  9034  mremre  16033  submre  16034  isacs1i  16087  eltg4i  20517  distop  20552  distopon  20553  distps  20571  ntrss2  20613  isopn3  20622  discld  20645  mretopd  20648  dishaus  20938  discmp  20953  dissnlocfin  21084  locfindis  21085  txdis  21187  xkopt  21210  xkofvcn  21239  hmphdis  21351  ustbas2  21781  vitali  23105  shsupcl  27387  shsupunss  27395  pwuniss  28559  iundifdifd  28568  iundifdif  28569  dispcmp  29060  mbfmcnt  29463  omssubadd  29495  carsgval  29498  carsggect  29513  coinflipprob  29674  coinflipuniv  29676  fnemeet2  31338  icoreunrn  32179  mapdunirnN  35753  ismrcd1  36075  hbt  36515  pwelg  36680  pwsal  39008  salgenval  39014  salgenn0  39022  salexct  39025  salgencntex  39034  0ome  39216  isomennd  39218  unidmovn  39300  rrnmbl  39301  hspmbl  39316
  Copyright terms: Public domain W3C validator