Theorem unipw 5410

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 4874	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4573	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1930	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4627	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5403	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4876	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 587	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2726	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  𝒫 cpw 4563  {csn 4589  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872

This theorem is referenced by:  univ  5411  pwtr  5412  unixpss  5773  pwexr  7741  unifpw  9306  fiuni  9379  ween  9988  fin23lem41  10305  mremre  17565  submre  17566  isacs1i  17618  eltg4i  22847  distop  22882  distopon  22884  distps  22902  ntrss2  22944  isopn3  22953  discld  22976  mretopd  22979  dishaus  23269  discmp  23285  dissnlocfin  23416  locfindis  23417  txdis  23519  xkopt  23542  xkofvcn  23571  hmphdis  23683  ustbas2  24113  vitali  25514  shsupcl  31267  shsupunss  31275  iundifdifd  32490  iundifdif  32491  dispcmp  33849  mbfmcnt  34259  omssubadd  34291  carsgval  34294  carsggect  34309  coinflipprob  34471  coinflipuniv  34473  fnemeet2  36355  bj-unirel  37039  bj-discrmoore  37099  icoreunrn  37347  ctbssinf  37394  mapdunirnN  41644  ismrcd1  42686  hbt  43119  pwelg  43549  pwsal  46313  salgenval  46319  salgenn0  46329  salexct  46332  salgencntex  46341  0ome  46527  isomennd  46529  unidmovn  46611  rrnmbl  46612  hspmbl  46627