Theorem unipw 5450

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 4911	. . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴))
2		elelpwi 4612	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
3	2	exlimiv 1932	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴)
4	1, 3	sylbi 216	. . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴)
5		vsnid 4665	. . . 4 ⊢ 𝑥 ∈ {𝑥}
6		snelpwi 5443	. . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴)
7		elunii 4913	. . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴)
8	5, 6, 7	sylancr 586	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴)
9	4, 8	impbii 208	. 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
10	9	eqriv 2728	1 ⊢ ∪ 𝒫 𝐴 = 𝐴

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1780   ∈ wcel 2105  𝒫 cpw 4602  {csn 4628  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953  df-in 3955  df-ss 3965  df-pw 4604  df-sn 4629  df-pr 4631  df-uni 4909

This theorem is referenced by:  univ  5451  pwtr  5452  unixpss  5810  pwexr  7756  unifpw  9359  fiuni  9427  ween  10034  fin23lem41  10351  mremre  17553  submre  17554  isacs1i  17606  eltg4i  22684  distop  22719  distopon  22721  distps  22740  ntrss2  22782  isopn3  22791  discld  22814  mretopd  22817  dishaus  23107  discmp  23123  dissnlocfin  23254  locfindis  23255  txdis  23357  xkopt  23380  xkofvcn  23409  hmphdis  23521  ustbas2  23951  vitali  25363  shsupcl  30859  shsupunss  30867  iundifdifd  32061  iundifdif  32062  dispcmp  33138  mbfmcnt  33566  omssubadd  33598  carsgval  33601  carsggect  33616  coinflipprob  33777  coinflipuniv  33779  fnemeet2  35556  bj-unirel  36236  bj-discrmoore  36296  icoreunrn  36544  ctbssinf  36591  mapdunirnN  40825  ismrcd1  41739  hbt  42175  pwelg  42614  pwsal  45330  salgenval  45336  salgenn0  45346  salexct  45349  salgencntex  45358  0ome  45544  isomennd  45546  unidmovn  45628  rrnmbl  45629  hspmbl  45644