Theorem unipw 5398

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 4854	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4552	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1932	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4608	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5392	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4856	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 588	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2734	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  𝒫 cpw 4542  {csn 4568  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  univ  5399  pwtr  5400  unixpss  5760  pwexr  7713  unifpw  9259  fiuni  9335  ween  9951  fin23lem41  10268  mremre  17560  submre  17561  isacs1i  17617  eltg4i  22938  distop  22973  distopon  22975  distps  22993  ntrss2  23035  isopn3  23044  discld  23067  mretopd  23070  dishaus  23360  discmp  23376  dissnlocfin  23507  locfindis  23508  txdis  23610  xkopt  23633  xkofvcn  23662  hmphdis  23774  ustbas2  24203  vitali  25593  shsupcl  31427  shsupunss  31435  iundifdifd  32649  iundifdif  32650  dispcmp  34022  mbfmcnt  34431  omssubadd  34463  carsgval  34466  carsggect  34481  coinflipprob  34643  coinflipuniv  34645  fnemeet2  36568  bj-unirel  37377  bj-discrmoore  37442  icoreunrn  37692  ctbssinf  37739  mapdunirnN  42113  ismrcd1  43147  hbt  43579  pwelg  44008  pwsal  46764  salgenval  46770  salgenn0  46780  salexct  46783  salgencntex  46792  0ome  46978  isomennd  46980  unidmovn  47062  rrnmbl  47063  hspmbl  47078