Theorem unisng 4860

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 4574	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4852	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4856	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 567	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4086	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2782	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ∪ cun 3885  {csn 4561  {cpr 4563  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564  df-uni 4840

This theorem is referenced by:  unisn  4861  unisn3  4862  dfnfc2  4863  unisn2  5236  en2other2  9765  pmtrprfv  19061  dprdsn  19639  indistopon  22151  ordtuni  22341  cmpcld  22553  ptcmplem5  23207  cldsubg  23262  icccmplem2  23986  vmappw  26265  chsupsn  29775  xrge0tsmseq  31319  cycpm2tr  31386  qustrivr  31561  esumsnf  32032  prsiga  32099  rossros  32148  cvmscld  33235  unisnif  34227  topjoin  34554  fnejoin2  34558  bj-snmoore  35284  pibt2  35588  heiborlem8  35976  nlimsuc  41048  fourierdlem80  43727