Theorem unipw 5418

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 4620	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5412	. . . 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 4584  ∪ 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 5391

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 3897  df-un 4150  df-pw 4558  df-sn 4585  df-pr 4587  df-uni 4867

This theorem is used by:  univ  5419  pwtr  5420  unixpss  5789  pwexr  7783  unifpw  9351  fiuni  9427  ween  10121  fin23lem41  10437  mremre  17783  submre  17784  isacs1i  17840  eltg4i  23287  distop  23322  distopon  23324  distps  23342  ntrss2  23384  isopn3  23393  discld  23416  mretopd  23419  dishaus  23709  discmp  23725  dissnlocfin  23857  locfindis  23858  txdis  23960  xkopt  23983  xkofvcn  24012  hmphdis  24124  ustbas2  24553  vitali  25943  shsupcl  31949  shsupunss  31957  iundifdifd  33207  iundifdif  33208  dispcmp  34541  mbfmcnt  34950  omssubadd  34982  carsgval  34985  carsggect  35000  coinflipprob  35162  coinflipuniv  35164  fnemeet2  37251  bj-unirel  38074  bj-discrmoore  38140  icoreunrn  38391  ctbssinf  38438  mapdunirnN  42816  ismrcd1  43818  hbt  44241  pwelg  44670  pwsal  47433  salgenval  47439  salgenn0  47449  salexct  47452  salgencntex  47461  0ome  47647  isomennd  47649  unidmovn  47731  rrnmbl  47732  hspmbl  47747  tmachlem-tpbase  48057  tmachlem-tpopen  48059