Theorem unisng 4881

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 4593	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4875	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4879	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4109	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2775	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∪ cun 3899  {csn 4580  {cpr 4582  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583  df-uni 4864

This theorem is referenced by:  unisn  4882  unisn3  4884  dfnfc2  4885  unisn2  5257  unisucs  6396  en2other2  9919  pmtrprfv  19382  dprdsn  19967  indistopon  22945  ordtuni  23134  cmpcld  23346  ptcmplem5  24000  cldsubg  24055  icccmplem2  24768  vmappw  27082  chsupsn  31488  xrge0tsmseq  33157  cycpm2tr  33201  qustrivr  33446  esumsnf  34221  prsiga  34288  rossros  34337  cvmscld  35467  unisnif  36117  topjoin  36559  fnejoin2  36563  bj-snmoore  37314  pibt2  37618  heiborlem8  38015  sucunisn  43609  onsucunitp  43611  oaun3  43620  fourierdlem80  46426