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 4868	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4566	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1932	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4622	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5399	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4870	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 588	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2734	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  𝒫 cpw 4556  {csn 4582  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  univ  5406  pwtr  5407  unixpss  5767  pwexr  7720  unifpw  9267  fiuni  9343  ween  9957  fin23lem41  10274  mremre  17535  submre  17536  isacs1i  17592  eltg4i  22916  distop  22951  distopon  22953  distps  22971  ntrss2  23013  isopn3  23022  discld  23045  mretopd  23048  dishaus  23338  discmp  23354  dissnlocfin  23485  locfindis  23486  txdis  23588  xkopt  23611  xkofvcn  23640  hmphdis  23752  ustbas2  24181  vitali  25582  shsupcl  31426  shsupunss  31434  iundifdifd  32648  iundifdif  32649  dispcmp  34037  mbfmcnt  34446  omssubadd  34478  carsgval  34481  carsggect  34496  coinflipprob  34658  coinflipuniv  34660  fnemeet2  36583  bj-unirel  37299  bj-discrmoore  37364  icoreunrn  37614  ctbssinf  37661  mapdunirnN  42026  ismrcd1  43055  hbt  43487  pwelg  43916  pwsal  46673  salgenval  46679  salgenn0  46689  salexct  46692  salgencntex  46701  0ome  46887  isomennd  46889  unidmovn  46971  rrnmbl  46972  hspmbl  46987