Theorem unipw 5405

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 4870	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4569	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1930	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4623	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5398	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4872	. . . 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 4559  {csn 4585  ∪ cuni 4867

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 5246  ax-pr 5382

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 3446  df-un 3916  df-ss 3928  df-pw 4561  df-sn 4586  df-pr 4588  df-uni 4868

This theorem is referenced by:  univ  5406  pwtr  5407  unixpss  5764  pwexr  7721  unifpw  9282  fiuni  9355  ween  9964  fin23lem41  10281  mremre  17541  submre  17542  isacs1i  17594  eltg4i  22823  distop  22858  distopon  22860  distps  22878  ntrss2  22920  isopn3  22929  discld  22952  mretopd  22955  dishaus  23245  discmp  23261  dissnlocfin  23392  locfindis  23393  txdis  23495  xkopt  23518  xkofvcn  23547  hmphdis  23659  ustbas2  24089  vitali  25490  shsupcl  31240  shsupunss  31248  iundifdifd  32463  iundifdif  32464  dispcmp  33822  mbfmcnt  34232  omssubadd  34264  carsgval  34267  carsggect  34282  coinflipprob  34444  coinflipuniv  34446  fnemeet2  36328  bj-unirel  37012  bj-discrmoore  37072  icoreunrn  37320  ctbssinf  37367  mapdunirnN  41617  ismrcd1  42659  hbt  43092  pwelg  43522  pwsal  46286  salgenval  46292  salgenn0  46302  salexct  46305  salgencntex  46314  0ome  46500  isomennd  46502  unidmovn  46584  rrnmbl  46585  hspmbl  46600