Theorem unipw 4845

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 4375	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4119	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1845	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 206	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4156	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 4839	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4377	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 694	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 198	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2607	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110  df-sn 4126  df-pr 4128  df-uni 4373

This theorem is referenced by:  univ  4846  pwtr  4848  unixpss  5157  pwexb  6867  unifpw  8152  fiuni  8217  ween  8741  fin23lem41  9057  mremre  16087  submre  16088  isacs1i  16141  eltg4i  20575  distop  20610  distopon  20611  distps  20629  ntrss2  20671  isopn3  20680  discld  20703  mretopd  20706  dishaus  20996  discmp  21011  dissnlocfin  21142  locfindis  21143  txdis  21245  xkopt  21268  xkofvcn  21297  hmphdis  21409  ustbas2  21839  vitali  23188  shsupcl  27581  shsupunss  27589  pwuniss  28753  iundifdifd  28762  iundifdif  28763  dispcmp  29254  mbfmcnt  29657  omssubadd  29689  carsgval  29692  carsggect  29707  coinflipprob  29868  coinflipuniv  29870  fnemeet2  31532  icoreunrn  32383  mapdunirnN  35957  ismrcd1  36279  hbt  36719  pwelg  36884  pwsal  39211  salgenval  39217  salgenn0  39225  salexct  39228  salgencntex  39237  0ome  39419  isomennd  39421  unidmovn  39503  rrnmbl  39504  hspmbl  39519