Theorem unisng 4929

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 4641	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4921	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4925	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 567	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4152	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2776	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ∪ cun 3946  {csn 4628  {cpr 4630  ∪ cuni 4908

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631  df-uni 4909

This theorem is referenced by:  unisn  4930  unisn3  4932  dfnfc2  4933  unisn2  5312  unisucs  6441  en2other2  10003  pmtrprfv  19320  dprdsn  19905  indistopon  22503  ordtuni  22693  cmpcld  22905  ptcmplem5  23559  cldsubg  23614  icccmplem2  24338  vmappw  26617  chsupsn  30661  xrge0tsmseq  32206  cycpm2tr  32273  qustrivr  32472  esumsnf  33057  prsiga  33124  rossros  33173  cvmscld  34259  unisnif  34892  topjoin  35245  fnejoin2  35249  bj-snmoore  35989  pibt2  36293  heiborlem8  36681  sucunisn  42111  onsucunitp  42113  oaun3  42122  fourierdlem80  44892