Theorem unipw 5432

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 4879	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4577	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1957	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 220	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4634	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5426	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4881	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 598	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 212	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2766	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  𝒫 cpw 4567  {csn 4594  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-pw 4569  df-sn 4595  df-pr 4597  df-uni 4877

This theorem is referenced by:  univ  5433  pwtr  5434  unixpss  5798  pwexr  7763  unifpw  9311  fiuni  9387  ween  10018  fin23lem41  10335  mremre  17655  submre  17656  isacs1i  17712  eltg4i  23085  distop  23120  distopon  23122  distps  23140  ntrss2  23182  isopn3  23191  discld  23214  mretopd  23217  dishaus  23507  discmp  23523  dissnlocfin  23654  locfindis  23655  txdis  23757  xkopt  23780  xkofvcn  23809  hmphdis  23921  ustbas2  24350  vitali  25740  shsupcl  31630  shsupunss  31638  iundifdifd  32846  iundifdif  32847  dispcmp  34193  mbfmcnt  34602  omssubadd  34634  carsgval  34637  carsggect  34652  coinflipprob  34814  coinflipuniv  34816  fnemeet2  36766  bj-unirel  37574  bj-discrmoore  37640  icoreunrn  37892  ctbssinf  37939  mapdunirnN  42313  ismrcd1  43320  hbt  43748  pwelg  44177  pwsal  46920  salgenval  46926  salgenn0  46936  salexct  46939  salgencntex  46948  0ome  47134  isomennd  47136  unidmovn  47218  rrnmbl  47219  hspmbl  47234