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

Theorem unipw 5105
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 4629 . . . 4 (𝑥 𝒫 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦 ∈ 𝒫 𝐴))
2 elelpwi 4361 . . . . 5 ((𝑥𝑦𝑦 ∈ 𝒫 𝐴) → 𝑥𝐴)
32exlimiv 2023 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ 𝒫 𝐴) → 𝑥𝐴)
41, 3sylbi 208 . . 3 (𝑥 𝒫 𝐴𝑥𝐴)
5 vsnid 4400 . . . 4 𝑥 ∈ {𝑥}
6 snelpwi 5099 . . . 4 (𝑥𝐴 → {𝑥} ∈ 𝒫 𝐴)
7 elunii 4631 . . . 4 ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 𝒫 𝐴)
85, 6, 7sylancr 577 . . 3 (𝑥𝐴𝑥 𝒫 𝐴)
94, 8impbii 200 . 2 (𝑥 𝒫 𝐴𝑥𝐴)
109eqriv 2802 1 𝒫 𝐴 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wex 1859  wcel 2158  𝒫 cpw 4348  {csn 4367   cuni 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-pw 4350  df-sn 4368  df-pr 4370  df-uni 4627
This theorem is referenced by:  univ  5106  pwtr  5108  unixpss  5432  pwexr  7201  unifpw  8505  fiuni  8570  ween  9138  fin23lem41  9456  mremre  16465  submre  16466  isacs1i  16518  eltg4i  20974  distop  21009  distopon  21011  distps  21029  ntrss2  21071  isopn3  21080  discld  21103  mretopd  21106  dishaus  21396  discmp  21411  dissnlocfin  21542  locfindis  21543  txdis  21645  xkopt  21668  xkofvcn  21697  hmphdis  21809  ustbas2  22238  vitali  23590  shsupcl  28522  shsupunss  28530  pwuniss  29692  iundifdifd  29702  iundifdif  29703  dispcmp  30248  mbfmcnt  30652  omssubadd  30684  carsgval  30687  carsggect  30702  coinflipprob  30863  coinflipuniv  30865  fnemeet2  32680  bj-discrmoore  33374  icoreunrn  33520  mapdunirnN  37428  ismrcd1  37760  hbt  38198  pwelg  38362  pwsal  41011  salgenval  41017  salgenn0  41025  salexct  41028  salgencntex  41037  0ome  41222  isomennd  41224  unidmovn  41306  rrnmbl  41307  hspmbl  41322
  Copyright terms: Public domain W3C validator