Theorem unisng 4895

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 4607	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4889	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4893	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 577	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4114	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2805	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ∪ cun 3906  {csn 4594  {cpr 4596  ∪ cuni 4877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-sn 4595  df-pr 4597  df-uni 4878

This theorem is used by:  unisn  4896  unisn3  4898  dfnfc2  4899  unisn2  5280  unisucs  6447  en2other2  10012  qustrivr  19284  pmtrprfv  19554  dprdsn  20139  indistopon  23195  ordtuni  23384  cmpcld  23596  ptcmplem5  24250  cldsubg  24305  icccmplem2  25018  vmappw  27317  chsupsn  31802  xrge0tsmseq  33426  cycpm2tr  33470  esumsnf  34485  prsiga  34552  rossros  34602  cvmscld  35786  unisnif  36436  topjoin  36917  fnejoin2  36921  bj-snmoore  37796  pibt2  38104  heiborlem8  38510  sucunisn  44139  onsucunitp  44141  oaun3  44150  fourierdlem80  46941