Theorem unisng 4886

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 4598	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4880	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4884	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 576	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4113	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2804	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145   ∪ cun 3905  {csn 4585  {cpr 4587  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588  df-uni 4869

This theorem is referenced by:  unisn  4887  unisn3  4889  dfnfc2  4890  unisn2  5267  unisucs  6429  en2other2  9981  qustrivr  19244  pmtrprfv  19514  dprdsn  20099  indistopon  23119  ordtuni  23308  cmpcld  23520  ptcmplem5  24174  cldsubg  24229  icccmplem2  24942  vmappw  27238  chsupsn  31674  xrge0tsmseq  33308  cycpm2tr  33352  esumsnf  34371  prsiga  34438  rossros  34487  cvmscld  35636  unisnif  36286  topjoin  36738  fnejoin2  36742  bj-snmoore  37615  pibt2  37923  heiborlem8  38329  sucunisn  43960  onsucunitp  43962  oaun3  43971  fourierdlem80  46758