Theorem unipw 5417

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 4869	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4566	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1962	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 220	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4623	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5411	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4871	. . . 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 1569  ∃wex 1811   ∈ wcel 2144  𝒫 cpw 4556  {csn 4583  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-pw 4558  df-sn 4584  df-pr 4586  df-uni 4867

This theorem is used by:  univ  5418  pwtr  5419  unixpss  5787  pwexr  7779  unifpw  9345  fiuni  9421  ween  10115  fin23lem41  10431  mremre  17775  submre  17776  isacs1i  17832  eltg4i  23279  distop  23314  distopon  23316  distps  23334  ntrss2  23376  isopn3  23385  discld  23408  mretopd  23411  dishaus  23701  discmp  23717  dissnlocfin  23849  locfindis  23850  txdis  23952  xkopt  23975  xkofvcn  24004  hmphdis  24116  ustbas2  24545  vitali  25935  shsupcl  31941  shsupunss  31949  iundifdifd  33199  iundifdif  33200  dispcmp  34534  mbfmcnt  34943  omssubadd  34975  carsgval  34978  carsggect  34993  coinflipprob  35155  coinflipuniv  35157  fnemeet2  37198  bj-unirel  38009  bj-discrmoore  38075  icoreunrn  38326  ctbssinf  38373  mapdunirnN  42751  ismrcd1  43753  hbt  44176  pwelg  44605  pwsal  47369  salgenval  47375  salgenn0  47385  salexct  47388  salgencntex  47397  0ome  47583  isomennd  47585  unidmovn  47667  rrnmbl  47668  hspmbl  47683  tmachlem-tpbase  47993  tmachlem-tpopen  47995