Theorem unisng 4905

Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)

Assertion

Ref	Expression
unisng	⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Proof of Theorem unisng

Step	Hyp	Ref	Expression
1		dfsn2 4619	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4899	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4903	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4137	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2773	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ∪ cun 3929  {csn 4606  {cpr 4608  ∪ cuni 4887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-un 3936  df-ss 3948  df-sn 4607  df-pr 4609  df-uni 4888

This theorem is referenced by:  unisn  4906  unisn3  4908  dfnfc2  4909  unisn2  5292  unisucs  6441  en2other2  10031  pmtrprfv  19439  dprdsn  20024  indistopon  22955  ordtuni  23144  cmpcld  23356  ptcmplem5  24010  cldsubg  24065  icccmplem2  24781  vmappw  27095  chsupsn  31360  xrge0tsmseq  33006  cycpm2tr  33078  qustrivr  33328  esumsnf  34024  prsiga  34091  rossros  34140  cvmscld  35237  unisnif  35885  topjoin  36325  fnejoin2  36329  bj-snmoore  37073  pibt2  37377  heiborlem8  37784  sucunisn  43346  onsucunitp  43348  oaun3  43357  fourierdlem80  46158