Theorem unipw 5433

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 4877	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4574	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1963	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 220	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4631	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5427	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4879	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 599	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 212	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2762	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  𝒫 cpw 4564  {csn 4591  ∪ cuni 4874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-pw 4566  df-sn 4592  df-pr 4594  df-uni 4875

This theorem is used by:  univ  5434  pwtr  5435  unixpss  5799  pwexr  7770  unifpw  9319  fiuni  9395  ween  10035  fin23lem41  10351  mremre  17678  submre  17679  isacs1i  17735  eltg4i  23167  distop  23202  distopon  23204  distps  23222  ntrss2  23264  isopn3  23273  discld  23296  mretopd  23299  dishaus  23589  discmp  23605  dissnlocfin  23737  locfindis  23738  txdis  23840  xkopt  23863  xkofvcn  23892  hmphdis  24004  ustbas2  24433  vitali  25823  shsupcl  31761  shsupunss  31769  iundifdifd  32977  iundifdif  32978  dispcmp  34313  mbfmcnt  34723  omssubadd  34755  carsgval  34758  carsggect  34773  coinflipprob  34935  coinflipuniv  34937  fnemeet2  36935  bj-unirel  37744  bj-discrmoore  37810  icoreunrn  38062  ctbssinf  38109  mapdunirnN  42482  ismrcd1  43487  hbt  43915  pwelg  44344  pwsal  47087  salgenval  47093  salgenn0  47103  salexct  47106  salgencntex  47115  0ome  47301  isomennd  47303  unidmovn  47385  rrnmbl  47386  hspmbl  47401