Theorem unisng 4930

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 4642	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4922	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4926	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 568	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4153	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2777	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ∪ cun 3947  {csn 4629  {cpr 4631  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632  df-uni 4910

This theorem is referenced by:  unisn  4931  unisn3  4933  dfnfc2  4934  unisn2  5313  unisucs  6442  en2other2  10004  pmtrprfv  19321  dprdsn  19906  indistopon  22504  ordtuni  22694  cmpcld  22906  ptcmplem5  23560  cldsubg  23615  icccmplem2  24339  vmappw  26620  chsupsn  30666  xrge0tsmseq  32211  cycpm2tr  32278  qustrivr  32477  esumsnf  33062  prsiga  33129  rossros  33178  cvmscld  34264  unisnif  34897  topjoin  35250  fnejoin2  35254  bj-snmoore  35994  pibt2  36298  heiborlem8  36686  sucunisn  42121  onsucunitp  42123  oaun3  42132  fourierdlem80  44902