Theorem unisng 4929

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 4643	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4923	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4927	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4166	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2778	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ∪ cun 3960  {csn 4630  {cpr 4632  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-sn 4631  df-pr 4633  df-uni 4912

This theorem is referenced by:  unisn  4930  unisn3  4932  dfnfc2  4933  unisn2  5317  unisucs  6462  en2other2  10046  pmtrprfv  19485  dprdsn  20070  indistopon  23023  ordtuni  23213  cmpcld  23425  ptcmplem5  24079  cldsubg  24134  icccmplem2  24858  vmappw  27173  chsupsn  31441  xrge0tsmseq  33049  cycpm2tr  33121  qustrivr  33372  esumsnf  34044  prsiga  34111  rossros  34160  cvmscld  35257  unisnif  35906  topjoin  36347  fnejoin2  36351  bj-snmoore  37095  pibt2  37399  heiborlem8  37804  sucunisn  43360  onsucunitp  43362  oaun3  43371  fourierdlem80  46141