Theorem unipw 5403

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 4854	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4552	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1932	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 217	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4608	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5397	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4856	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 588	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 209	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2734	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  𝒫 cpw 4542  {csn 4568  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  univ  5404  pwtr  5405  unixpss  5766  pwexr  7719  unifpw  9265  fiuni  9341  ween  9957  fin23lem41  10274  mremre  17566  submre  17567  isacs1i  17623  eltg4i  22925  distop  22960  distopon  22962  distps  22980  ntrss2  23022  isopn3  23031  discld  23054  mretopd  23057  dishaus  23347  discmp  23363  dissnlocfin  23494  locfindis  23495  txdis  23597  xkopt  23620  xkofvcn  23649  hmphdis  23761  ustbas2  24190  vitali  25580  shsupcl  31409  shsupunss  31417  iundifdifd  32631  iundifdif  32632  dispcmp  34003  mbfmcnt  34412  omssubadd  34444  carsgval  34447  carsggect  34462  coinflipprob  34624  coinflipuniv  34626  fnemeet2  36549  bj-unirel  37358  bj-discrmoore  37423  icoreunrn  37675  ctbssinf  37722  mapdunirnN  42096  ismrcd1  43130  hbt  43558  pwelg  43987  pwsal  46743  salgenval  46749  salgenn0  46759  salexct  46762  salgencntex  46771  0ome  46957  isomennd  46959  unidmovn  47041  rrnmbl  47042  hspmbl  47057