Theorem unipw 4948

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 4471	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4204	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1898	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 207	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4242	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 4942	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4473	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 696	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 199	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2648	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030  𝒫 cpw 4191  {csn 4210  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-pw 4193  df-sn 4211  df-pr 4213  df-uni 4469

This theorem is referenced by:  univ  4949  pwtr  4951  unixpss  5267  pwexr  7016  unifpw  8310  fiuni  8375  ween  8896  fin23lem41  9212  mremre  16311  submre  16312  isacs1i  16365  eltg4i  20812  distop  20847  distopon  20849  distps  20867  ntrss2  20909  isopn3  20918  discld  20941  mretopd  20944  dishaus  21234  discmp  21249  dissnlocfin  21380  locfindis  21381  txdis  21483  xkopt  21506  xkofvcn  21535  hmphdis  21647  ustbas2  22076  vitali  23427  shsupcl  28325  shsupunss  28333  pwuniss  29496  iundifdifd  29506  iundifdif  29507  dispcmp  30054  mbfmcnt  30458  omssubadd  30490  carsgval  30493  carsggect  30508  coinflipprob  30669  coinflipuniv  30671  fnemeet2  32487  bj-discrmoore  33191  icoreunrn  33337  mapdunirnN  37256  ismrcd1  37578  hbt  38017  pwelg  38182  pwsal  40853  salgenval  40859  salgenn0  40867  salexct  40870  salgencntex  40879  0ome  41064  isomennd  41066  unidmovn  41148  rrnmbl  41149  hspmbl  41164