Theorem unipw 5396

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 4864	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4562	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1931	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4618	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5390	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4866	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 587	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2731	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  𝒫 cpw 4552  {csn 4578  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-pw 4554  df-sn 4579  df-pr 4581  df-uni 4862

This theorem is referenced by:  univ  5397  pwtr  5398  unixpss  5757  pwexr  7708  unifpw  9253  fiuni  9329  ween  9943  fin23lem41  10260  mremre  17521  submre  17522  isacs1i  17578  eltg4i  22902  distop  22937  distopon  22939  distps  22957  ntrss2  22999  isopn3  23008  discld  23031  mretopd  23034  dishaus  23324  discmp  23340  dissnlocfin  23471  locfindis  23472  txdis  23574  xkopt  23597  xkofvcn  23626  hmphdis  23738  ustbas2  24167  vitali  25568  shsupcl  31362  shsupunss  31370  iundifdifd  32585  iundifdif  32586  dispcmp  33965  mbfmcnt  34374  omssubadd  34406  carsgval  34409  carsggect  34424  coinflipprob  34586  coinflipuniv  34588  fnemeet2  36510  bj-unirel  37195  bj-discrmoore  37255  icoreunrn  37503  ctbssinf  37550  mapdunirnN  41849  ismrcd1  42882  hbt  43314  pwelg  43743  pwsal  46501  salgenval  46507  salgenn0  46517  salexct  46520  salgencntex  46529  0ome  46715  isomennd  46717  unidmovn  46799  rrnmbl  46800  hspmbl  46815