Theorem unipw 4918

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 4439	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4171	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1858	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 207	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4209	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 4912	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4441	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 695	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 199	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2619	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  𝒫 cpw 4158  {csn 4177  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437

This theorem is referenced by:  univ  4919  pwtr  4921  unixpss  5234  pwexr  6974  unifpw  8269  fiuni  8334  ween  8858  fin23lem41  9174  mremre  16264  submre  16265  isacs1i  16318  eltg4i  20764  distop  20799  distopon  20801  distps  20819  ntrss2  20861  isopn3  20870  discld  20893  mretopd  20896  dishaus  21186  discmp  21201  dissnlocfin  21332  locfindis  21333  txdis  21435  xkopt  21458  xkofvcn  21487  hmphdis  21599  ustbas2  22029  vitali  23382  shsupcl  28197  shsupunss  28205  pwuniss  29370  iundifdifd  29380  iundifdif  29381  dispcmp  29926  mbfmcnt  30330  omssubadd  30362  carsgval  30365  carsggect  30380  coinflipprob  30541  coinflipuniv  30543  fnemeet2  32362  bj-discrmoore  33066  icoreunrn  33207  mapdunirnN  36939  ismrcd1  37261  hbt  37700  pwelg  37865  pwsal  40535  salgenval  40541  salgenn0  40549  salexct  40552  salgencntex  40561  0ome  40743  isomennd  40745  unidmovn  40827  rrnmbl  40828  hspmbl  40843