Theorem unisng 4888

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 4600	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4882	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4886	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 577	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4107	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2801	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∪ cun 3900  {csn 4587  {cpr 4589  ∪ cuni 4870

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-sn 4588  df-pr 4590  df-uni 4871

This theorem is used by:  unisn  4889  unisn3  4891  dfnfc2  4892  unisn2  5273  unisucs  6441  en2other2  10016  qustrivr  19316  pmtrprfv  19586  dprdsn  20171  indistopon  23232  ordtuni  23421  cmpcld  23633  ptcmplem5  24288  cldsubg  24343  icccmplem2  25056  vmappw  27360  chsupsn  31902  xrge0tsmseq  33523  cycpm2tr  33567  esumsnf  34582  prsiga  34649  rossros  34699  cvmscld  35860  unisnif  36510  topjoin  36992  fnejoin2  36996  bj-snmoore  37871  pibt2  38179  heiborlem8  38576  sucunisn  44220  onsucunitp  44222  oaun3  44231  fourierdlem80  47022