Theorem unisng 4868

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∪ cun 3887  {csn 4567  {cpr 4569  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  unisn  4869  unisn3  4871  dfnfc2  4872  unisn2  5247  unisucs  6402  en2other2  9931  pmtrprfv  19428  dprdsn  20013  indistopon  22966  ordtuni  23155  cmpcld  23367  ptcmplem5  24021  cldsubg  24076  icccmplem2  24789  vmappw  27079  chsupsn  31484  xrge0tsmseq  33136  cycpm2tr  33180  qustrivr  33425  esumsnf  34208  prsiga  34275  rossros  34324  cvmscld  35455  unisnif  36105  topjoin  36547  fnejoin2  36551  bj-snmoore  37425  pibt2  37733  heiborlem8  38139  sucunisn  43799  onsucunitp  43801  oaun3  43810  fourierdlem80  46614