Theorem unipw 5398

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

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  𝒫 cpw 4554  {csn 4580  ∪ cuni 4863

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 2708  ax-sep 5241  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pw 4556  df-sn 4581  df-pr 4583  df-uni 4864

This theorem is referenced by:  univ  5399  pwtr  5400  unixpss  5759  pwexr  7710  unifpw  9255  fiuni  9331  ween  9945  fin23lem41  10262  mremre  17523  submre  17524  isacs1i  17580  eltg4i  22904  distop  22939  distopon  22941  distps  22959  ntrss2  23001  isopn3  23010  discld  23033  mretopd  23036  dishaus  23326  discmp  23342  dissnlocfin  23473  locfindis  23474  txdis  23576  xkopt  23599  xkofvcn  23628  hmphdis  23740  ustbas2  24169  vitali  25570  shsupcl  31413  shsupunss  31421  iundifdifd  32636  iundifdif  32637  dispcmp  34016  mbfmcnt  34425  omssubadd  34457  carsgval  34460  carsggect  34475  coinflipprob  34637  coinflipuniv  34639  fnemeet2  36561  bj-unirel  37252  bj-discrmoore  37316  icoreunrn  37564  ctbssinf  37611  mapdunirnN  41910  ismrcd1  42940  hbt  43372  pwelg  43801  pwsal  46559  salgenval  46565  salgenn0  46575  salexct  46578  salgencntex  46587  0ome  46773  isomennd  46775  unidmovn  46857  rrnmbl  46858  hspmbl  46873