Theorem unipw 5430

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  𝒫 cpw 4580  {csn 4606  ∪ cuni 4888

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 2708  ax-sep 5271  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948  df-pw 4582  df-sn 4607  df-pr 4609  df-uni 4889

This theorem is referenced by:  univ  5431  pwtr  5432  unixpss  5794  pwexr  7764  unifpw  9372  fiuni  9445  ween  10054  fin23lem41  10371  mremre  17621  submre  17622  isacs1i  17674  eltg4i  22903  distop  22938  distopon  22940  distps  22958  ntrss2  23000  isopn3  23009  discld  23032  mretopd  23035  dishaus  23325  discmp  23341  dissnlocfin  23472  locfindis  23473  txdis  23575  xkopt  23598  xkofvcn  23627  hmphdis  23739  ustbas2  24169  vitali  25571  shsupcl  31324  shsupunss  31332  iundifdifd  32547  iundifdif  32548  dispcmp  33895  mbfmcnt  34305  omssubadd  34337  carsgval  34340  carsggect  34355  coinflipprob  34517  coinflipuniv  34519  fnemeet2  36390  bj-unirel  37074  bj-discrmoore  37134  icoreunrn  37382  ctbssinf  37429  mapdunirnN  41674  ismrcd1  42688  hbt  43121  pwelg  43551  pwsal  46311  salgenval  46317  salgenn0  46327  salexct  46330  salgencntex  46339  0ome  46525  isomennd  46527  unidmovn  46609  rrnmbl  46610  hspmbl  46625