Theorem unipw 5366

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 4842	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4545	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1933	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 216	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4598	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5360	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4844	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 587	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 208	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2735	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-pw 4535  df-sn 4562  df-pr 4564  df-uni 4840

This theorem is referenced by:  univ  5367  pwtr  5368  unixpss  5720  pwexr  7615  unifpw  9122  fiuni  9187  ween  9791  fin23lem41  10108  mremre  17313  submre  17314  isacs1i  17366  eltg4i  22110  distop  22145  distopon  22147  distps  22166  ntrss2  22208  isopn3  22217  discld  22240  mretopd  22243  dishaus  22533  discmp  22549  dissnlocfin  22680  locfindis  22681  txdis  22783  xkopt  22806  xkofvcn  22835  hmphdis  22947  ustbas2  23377  vitali  24777  shsupcl  29700  shsupunss  29708  iundifdifd  30901  iundifdif  30902  dispcmp  31809  mbfmcnt  32235  omssubadd  32267  carsgval  32270  carsggect  32285  coinflipprob  32446  coinflipuniv  32448  fnemeet2  34556  bj-unirel  35224  bj-discrmoore  35282  icoreunrn  35530  ctbssinf  35577  mapdunirnN  39664  ismrcd1  40520  hbt  40955  pwelg  41167  pwsal  43856  salgenval  43862  salgenn0  43870  salexct  43873  salgencntex  43882  0ome  44067  isomennd  44069  unidmovn  44151  rrnmbl  44152  hspmbl  44167