Theorem unipw 5470

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 4934	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4632	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1929	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4685	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5463	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4936	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 586	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2737	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  𝒫 cpw 4622  {csn 4648  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-pw 4624  df-sn 4649  df-pr 4651  df-uni 4932

This theorem is referenced by:  univ  5471  pwtr  5472  unixpss  5834  pwexr  7800  unifpw  9425  fiuni  9497  ween  10104  fin23lem41  10421  mremre  17662  submre  17663  isacs1i  17715  eltg4i  22988  distop  23023  distopon  23025  distps  23044  ntrss2  23086  isopn3  23095  discld  23118  mretopd  23121  dishaus  23411  discmp  23427  dissnlocfin  23558  locfindis  23559  txdis  23661  xkopt  23684  xkofvcn  23713  hmphdis  23825  ustbas2  24255  vitali  25667  shsupcl  31370  shsupunss  31378  iundifdifd  32584  iundifdif  32585  dispcmp  33805  mbfmcnt  34233  omssubadd  34265  carsgval  34268  carsggect  34283  coinflipprob  34444  coinflipuniv  34446  fnemeet2  36333  bj-unirel  37017  bj-discrmoore  37077  icoreunrn  37325  ctbssinf  37372  mapdunirnN  41607  ismrcd1  42654  hbt  43087  pwelg  43522  pwsal  46236  salgenval  46242  salgenn0  46252  salexct  46255  salgencntex  46264  0ome  46450  isomennd  46452  unidmovn  46534  rrnmbl  46535  hspmbl  46550