Theorem unipw 5402

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  𝒫 cpw 4541  {csn 4567  ∪ cuni 4850

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pw 4543  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  univ  5403  pwtr  5404  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