Theorem unipw 5389

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 4841	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4539	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1937	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 218	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4595	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5383	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4843	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 593	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 210	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2736	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  𝒫 cpw 4529  {csn 4555  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-pw 4531  df-sn 4556  df-pr 4558  df-uni 4839

This theorem is referenced by:  univ  5390  pwtr  5391  unixpss  5753  pwexr  7708  unifpw  9255  fiuni  9331  ween  9948  fin23lem41  10265  mremre  17557  submre  17558  isacs1i  17614  eltg4i  22943  distop  22978  distopon  22980  distps  22998  ntrss2  23040  isopn3  23049  discld  23072  mretopd  23075  dishaus  23365  discmp  23381  dissnlocfin  23512  locfindis  23513  txdis  23615  xkopt  23638  xkofvcn  23667  hmphdis  23779  ustbas2  24208  vitali  25598  shsupcl  31427  shsupunss  31435  iundifdifd  32650  iundifdif  32651  dispcmp  34043  mbfmcnt  34452  omssubadd  34484  carsgval  34487  carsggect  34502  coinflipprob  34664  coinflipuniv  34666  fnemeet2  36595  bj-unirel  37404  bj-discrmoore  37469  icoreunrn  37721  ctbssinf  37768  mapdunirnN  42142  ismrcd1  43147  hbt  43575  pwelg  44004  pwsal  46758  salgenval  46764  salgenn0  46774  salexct  46777  salgencntex  46786  0ome  46972  isomennd  46974  unidmovn  47056  rrnmbl  47057  hspmbl  47072