Theorem unisng 4889

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 4602	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4883	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4887	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4120	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2768	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∪ cun 3912  {csn 4589  {cpr 4591  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592  df-uni 4872

This theorem is referenced by:  unisn  4890  unisn3  4892  dfnfc2  4893  unisn2  5267  unisucs  6411  en2other2  9962  pmtrprfv  19383  dprdsn  19968  indistopon  22888  ordtuni  23077  cmpcld  23289  ptcmplem5  23943  cldsubg  23998  icccmplem2  24712  vmappw  27026  chsupsn  31342  xrge0tsmseq  33004  cycpm2tr  33076  qustrivr  33336  esumsnf  34054  prsiga  34121  rossros  34170  cvmscld  35260  unisnif  35913  topjoin  36353  fnejoin2  36357  bj-snmoore  37101  pibt2  37405  heiborlem8  37812  sucunisn  43360  onsucunitp  43362  oaun3  43371  fourierdlem80  46184