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  30697  xrge0tsmseq  32242  cycpm2tr  32309  qustrivr  32508  esumsnf  33093  prsiga  33160  rossros  33209  cvmscld  34295  unisnif  34928  topjoin  35298  fnejoin2  35302  bj-snmoore  36042  pibt2  36346  heiborlem8  36734  sucunisn  42169  onsucunitp  42171  oaun3  42180  fourierdlem80  44950