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

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  univ  5419  pwtr  5420  unixpss  5788  pwexr  7777  unifpw  9337  fiuni  9413  ween  10107  fin23lem41  10423  mremre  17767  submre  17768  isacs1i  17824  eltg4i  23271  distop  23306  distopon  23308  distps  23326  ntrss2  23368  isopn3  23377  discld  23400  mretopd  23403  dishaus  23693  discmp  23709  dissnlocfin  23841  locfindis  23842  txdis  23944  xkopt  23967  xkofvcn  23996  hmphdis  24108  ustbas2  24537  vitali  25927  shsupcl  31933  shsupunss  31941  iundifdifd  33149  iundifdif  33150  dispcmp  34484  mbfmcnt  34893  omssubadd  34925  carsgval  34928  carsggect  34943  coinflipprob  35105  coinflipuniv  35107  fnemeet2  37135  bj-unirel  37946  bj-discrmoore  38012  icoreunrn  38262  ctbssinf  38309  mapdunirnN  42687  ismrcd1  43688  hbt  44116  pwelg  44545  pwsal  47294  salgenval  47300  salgenn0  47310  salexct  47313  salgencntex  47322  0ome  47508  isomennd  47510  unidmovn  47592  rrnmbl  47593  hspmbl  47608  tmachlem-tpbase  47918  tmachlem-tpopen  47920