Theorem unipw 5431

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 4572	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1960	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 220	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4629	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5425	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4877	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 598	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 212	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2760	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  𝒫 cpw 4562  {csn 4589  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-pw 4564  df-sn 4590  df-pr 4592  df-uni 4873

This theorem is referenced by:  univ  5432  pwtr  5433  unixpss  5797  pwexr  7760  unifpw  9308  fiuni  9384  ween  10015  fin23lem41  10331  mremre  17651  submre  17652  isacs1i  17708  eltg4i  23117  distop  23152  distopon  23154  distps  23172  ntrss2  23214  isopn3  23223  discld  23246  mretopd  23249  dishaus  23539  discmp  23555  dissnlocfin  23686  locfindis  23687  txdis  23789  xkopt  23812  xkofvcn  23841  hmphdis  23953  ustbas2  24382  vitali  25772  shsupcl  31690  shsupunss  31698  iundifdifd  32906  iundifdif  32907  dispcmp  34249  mbfmcnt  34658  omssubadd  34690  carsgval  34693  carsggect  34708  coinflipprob  34870  coinflipuniv  34872  fnemeet2  36878  bj-unirel  37687  bj-discrmoore  37753  icoreunrn  38005  ctbssinf  38052  mapdunirnN  42424  ismrcd1  43429  hbt  43857  pwelg  44286  pwsal  47029  salgenval  47035  salgenn0  47045  salexct  47048  salgencntex  47057  0ome  47243  isomennd  47245  unidmovn  47327  rrnmbl  47328  hspmbl  47343