Theorem unipw 5360

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 4839	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4542	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1934	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 216	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4595	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5354	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4841	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 586	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 208	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2735	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  𝒫 cpw 4530  {csn 4558  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561  df-uni 4837

This theorem is referenced by:  univ  5361  pwtr  5362  unixpss  5709  pwexr  7593  unifpw  9052  fiuni  9117  ween  9722  fin23lem41  10039  mremre  17230  submre  17231  isacs1i  17283  eltg4i  22018  distop  22053  distopon  22055  distps  22074  ntrss2  22116  isopn3  22125  discld  22148  mretopd  22151  dishaus  22441  discmp  22457  dissnlocfin  22588  locfindis  22589  txdis  22691  xkopt  22714  xkofvcn  22743  hmphdis  22855  ustbas2  23285  vitali  24682  shsupcl  29601  shsupunss  29609  iundifdifd  30802  iundifdif  30803  dispcmp  31711  mbfmcnt  32135  omssubadd  32167  carsgval  32170  carsggect  32185  coinflipprob  32346  coinflipuniv  32348  fnemeet2  34483  bj-unirel  35151  bj-discrmoore  35209  icoreunrn  35457  ctbssinf  35504  mapdunirnN  39591  ismrcd1  40436  hbt  40871  pwelg  41056  pwsal  43746  salgenval  43752  salgenn0  43760  salexct  43763  salgencntex  43772  0ome  43957  isomennd  43959  unidmovn  44041  rrnmbl  44042  hspmbl  44057