Theorem unipw 5435

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

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  𝒫 cpw 4580  {csn 4606  ∪ cuni 4887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-un 3936  df-ss 3948  df-pw 4582  df-sn 4607  df-pr 4609  df-uni 4888

This theorem is referenced by:  univ  5436  pwtr  5437  unixpss  5800  pwexr  7767  unifpw  9377  fiuni  9450  ween  10057  fin23lem41  10374  mremre  17619  submre  17620  isacs1i  17672  eltg4i  22915  distop  22950  distopon  22952  distps  22970  ntrss2  23012  isopn3  23021  discld  23044  mretopd  23047  dishaus  23337  discmp  23353  dissnlocfin  23484  locfindis  23485  txdis  23587  xkopt  23610  xkofvcn  23639  hmphdis  23751  ustbas2  24181  vitali  25585  shsupcl  31286  shsupunss  31294  iundifdifd  32510  iundifdif  32511  dispcmp  33833  mbfmcnt  34245  omssubadd  34277  carsgval  34280  carsggect  34295  coinflipprob  34457  coinflipuniv  34459  fnemeet2  36343  bj-unirel  37027  bj-discrmoore  37087  icoreunrn  37335  ctbssinf  37382  mapdunirnN  41627  ismrcd1  42687  hbt  43120  pwelg  43550  pwsal  46302  salgenval  46308  salgenn0  46318  salexct  46321  salgencntex  46330  0ome  46516  isomennd  46518  unidmovn  46600  rrnmbl  46601  hspmbl  46616