Theorem unipw 5425

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  univ  5426  pwtr  5427  unixpss  5791  pwexr  7764  unifpw  9322  fiuni  9398  ween  10038  fin23lem41  10354  mremre  17688  submre  17689  isacs1i  17745  eltg4i  23185  distop  23220  distopon  23222  distps  23240  ntrss2  23282  isopn3  23291  discld  23314  mretopd  23317  dishaus  23607  discmp  23623  dissnlocfin  23755  locfindis  23756  txdis  23858  xkopt  23881  xkofvcn  23910  hmphdis  24022  ustbas2  24451  vitali  25841  shsupcl  31819  shsupunss  31827  iundifdifd  33035  iundifdif  33036  dispcmp  34369  mbfmcnt  34779  omssubadd  34811  carsgval  34814  carsggect  34829  coinflipprob  34991  coinflipuniv  34993  fnemeet2  36986  bj-unirel  37795  bj-discrmoore  37861  icoreunrn  38113  ctbssinf  38160  mapdunirnN  42523  ismrcd1  43543  hbt  43971  pwelg  44400  pwsal  47143  salgenval  47149  salgenn0  47159  salexct  47162  salgencntex  47171  0ome  47357  isomennd  47359  unidmovn  47441  rrnmbl  47442  hspmbl  47457  tmachlem-tpbase  47767  tmachlem-tpopen  47769