Theorem unipw 5393

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.

Step	Hyp	Ref	Expression
1		eluni 4861	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4561	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1930	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4615	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5386	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4863	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 587	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2726	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  𝒫 cpw 4551  {csn 4577  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4859

This theorem is referenced by:  univ  5394  pwtr  5395  unixpss  5753  pwexr  7701  unifpw  9245  fiuni  9318  ween  9929  fin23lem41  10246  mremre  17506  submre  17507  isacs1i  17563  eltg4i  22845  distop  22880  distopon  22882  distps  22900  ntrss2  22942  isopn3  22951  discld  22974  mretopd  22977  dishaus  23267  discmp  23283  dissnlocfin  23414  locfindis  23415  txdis  23517  xkopt  23540  xkofvcn  23569  hmphdis  23681  ustbas2  24111  vitali  25512  shsupcl  31282  shsupunss  31290  iundifdifd  32505  iundifdif  32506  dispcmp  33826  mbfmcnt  34236  omssubadd  34268  carsgval  34271  carsggect  34286  coinflipprob  34448  coinflipuniv  34450  fnemeet2  36341  bj-unirel  37025  bj-discrmoore  37085  icoreunrn  37333  ctbssinf  37380  mapdunirnN  41629  ismrcd1  42671  hbt  43103  pwelg  43533  pwsal  46296  salgenval  46302  salgenn0  46312  salexct  46315  salgencntex  46324  0ome  46510  isomennd  46512  unidmovn  46594  rrnmbl  46595  hspmbl  46610