Theorem unipw 5417

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 4868	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4565	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1950	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 219	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4622	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5411	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4870	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 596	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 211	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2759	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 399   = wceq 1560  ∃wex 1799   ∈ wcel 2142  𝒫 cpw 4555  {csn 4582  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-pw 4557  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  univ  5418  pwtr  5419  unixpss  5783  pwexr  7748  unifpw  9298  fiuni  9374  ween  9991  fin23lem41  10309  mremre  17632  submre  17633  isacs1i  17689  eltg4i  23017  distop  23052  distopon  23054  distps  23072  ntrss2  23114  isopn3  23123  discld  23146  mretopd  23149  dishaus  23439  discmp  23455  dissnlocfin  23586  locfindis  23587  txdis  23689  xkopt  23712  xkofvcn  23741  hmphdis  23853  ustbas2  24282  vitali  25672  shsupcl  31538  shsupunss  31546  iundifdifd  32758  iundifdif  32759  dispcmp  34153  mbfmcnt  34562  omssubadd  34594  carsgval  34597  carsggect  34612  coinflipprob  34774  coinflipuniv  34776  fnemeet2  36724  bj-unirel  37533  bj-discrmoore  37598  icoreunrn  37850  ctbssinf  37897  mapdunirnN  42271  ismrcd1  43276  hbt  43704  pwelg  44133  pwsal  46886  salgenval  46892  salgenn0  46902  salexct  46905  salgencntex  46914  0ome  47100  isomennd  47102  unidmovn  47184  rrnmbl  47185  hspmbl  47200