Theorem unipw 5308

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 4803	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4509	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1931	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 220	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4562	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5302	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4805	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 590	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 212	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2795	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  𝒫 cpw 4497  {csn 4525  ∪ cuni 4800

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

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 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528  df-uni 4801

This theorem is referenced by:  univ  5309  pwtr  5310  unixpss  5647  pwexr  7467  unifpw  8811  fiuni  8876  ween  9446  fin23lem41  9763  mremre  16867  submre  16868  isacs1i  16920  eltg4i  21565  distop  21600  distopon  21602  distps  21620  ntrss2  21662  isopn3  21671  discld  21694  mretopd  21697  dishaus  21987  discmp  22003  dissnlocfin  22134  locfindis  22135  txdis  22237  xkopt  22260  xkofvcn  22289  hmphdis  22401  ustbas2  22831  vitali  24217  shsupcl  29121  shsupunss  29129  iundifdifd  30325  iundifdif  30326  dispcmp  31212  mbfmcnt  31636  omssubadd  31668  carsgval  31671  carsggect  31686  coinflipprob  31847  coinflipuniv  31849  fnemeet2  33828  bj-unirel  34468  bj-discrmoore  34526  icoreunrn  34776  ctbssinf  34823  mapdunirnN  38946  ismrcd1  39639  hbt  40074  pwelg  40259  pwsal  42957  salgenval  42963  salgenn0  42971  salexct  42974  salgencntex  42983  0ome  43168  isomennd  43170  unidmovn  43252  rrnmbl  43253  hspmbl  43268