Theorem unisng 4877

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 4589	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4871	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4875	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 573	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4105	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2795	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136   ∪ cun 3897  {csn 4576  {cpr 4578  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-v 3450  df-un 3904  df-ss 3916  df-sn 4577  df-pr 4579  df-uni 4860

This theorem is referenced by:  unisn  4878  unisn3  4880  dfnfc2  4881  unisn2  5256  unisucs  6414  en2other2  9955  pmtrprfv  19469  dprdsn  20054  indistopon  23034  ordtuni  23223  cmpcld  23435  ptcmplem5  24089  cldsubg  24144  icccmplem2  24857  vmappw  27150  chsupsn  31555  xrge0tsmseq  33209  cycpm2tr  33253  qustrivr  33505  esumsnf  34315  prsiga  34382  rossros  34431  cvmscld  35571  unisnif  36221  topjoin  36673  fnejoin2  36677  bj-snmoore  37551  pibt2  37859  heiborlem8  38265  sucunisn  43896  onsucunitp  43898  oaun3  43907  fourierdlem80  46708