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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  𝒫 cpw 4560  {csn 4588  ∪ cuni 4872

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pw 4562  df-sn 4589  df-pr 4591  df-uni 4873

This theorem is used by:  univ  5426  pwtr  5427  unixpss  5797  pwexr  7811  unifpw  9382  fiuni  9457  ween  10153  fin23lem41  10469  mremre  17824  submre  17825  isacs1i  17881  eltg4i  23333  distop  23368  distopon  23370  distps  23388  ntrss2  23430  isopn3  23439  discld  23462  mretopd  23465  dishaus  23755  discmp  23771  dissnlocfin  23903  locfindis  23904  txdis  24006  xkopt  24029  xkofvcn  24058  hmphdis  24170  ustbas2  24599  vitali  25989  shsupcl  31997  shsupunss  32005  iundifdifd  33254  iundifdif  33255  dispcmp  34602  mbfmcnt  35011  omssubadd  35043  carsgval  35046  carsggect  35061  coinflipprob  35223  coinflipuniv  35225  fnemeet2  37370  bj-unirel  38236  bj-discrmoore  38302  icoreunrn  38550  ctbssinf  38597  mapdunirnN  42973  ismrcd1  43975  hbt  44397  pwelg  44822  pwsal  47598  salgenval  47604  salgenn0  47614  salexct  47617  salgencntex  47626  0ome  47812  isomennd  47814  unidmovn  47896  rrnmbl  47897  hspmbl  47912  tmachlem-tpbase  48222  tmachlem-tpopen  48224