Theorem unisng 4869

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 4581	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4863	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4867	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4098	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2776	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∪ cun 3888  {csn 4568  {cpr 4570  ∪ cuni 4851

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  unisn  4870  unisn3  4872  dfnfc2  4873  unisn2  5247  unisucs  6396  en2other2  9922  pmtrprfv  19419  dprdsn  20004  indistopon  22976  ordtuni  23165  cmpcld  23377  ptcmplem5  24031  cldsubg  24086  icccmplem2  24799  vmappw  27093  chsupsn  31499  xrge0tsmseq  33151  cycpm2tr  33195  qustrivr  33440  esumsnf  34224  prsiga  34291  rossros  34340  cvmscld  35471  unisnif  36121  topjoin  36563  fnejoin2  36567  bj-snmoore  37441  pibt2  37747  heiborlem8  38153  sucunisn  43817  onsucunitp  43819  oaun3  43828  fourierdlem80  46632