Theorem unisng 4827

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 4539	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4819	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4823	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 570	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4052	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2778	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∪ cun 3851  {csn 4526  {cpr 4528  ∪ cuni 4806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-in 3860  df-ss 3870  df-sn 4527  df-pr 4529  df-uni 4807

This theorem is referenced by:  unisn  4828  unisn3  4829  dfnfc2  4830  unisn2  5190  en2other2  9522  pmtrprfv  18712  dprdsn  19290  indistopon  21765  ordtuni  21954  cmpcld  22166  ptcmplem5  22820  cldsubg  22875  icccmplem2  23588  vmappw  25866  chsupsn  29361  xrge0tsmseq  30909  cycpm2tr  30976  qustrivr  31146  esumsnf  31615  prsiga  31682  rossros  31731  cvmscld  32819  unisnif  33883  topjoin  34210  fnejoin2  34214  bj-snmoore  34938  pibt2  35244  heiborlem8  35632  fourierdlem80  43310