Theorem unisng 4879

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 4592	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4873	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4877	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4110	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2768	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∪ cun 3903  {csn 4579  {cpr 4581  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-sn 4580  df-pr 4582  df-uni 4862

This theorem is referenced by:  unisn  4880  unisn3  4882  dfnfc2  4883  unisn2  5254  unisucs  6390  en2other2  9922  pmtrprfv  19350  dprdsn  19935  indistopon  22904  ordtuni  23093  cmpcld  23305  ptcmplem5  23959  cldsubg  24014  icccmplem2  24728  vmappw  27042  chsupsn  31375  xrge0tsmseq  33030  cycpm2tr  33074  qustrivr  33312  esumsnf  34030  prsiga  34097  rossros  34146  cvmscld  35245  unisnif  35898  topjoin  36338  fnejoin2  36342  bj-snmoore  37086  pibt2  37390  heiborlem8  37797  sucunisn  43344  onsucunitp  43346  oaun3  43355  fourierdlem80  46168