Theorem unisng 4888

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 4597	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4882	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4886	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 577	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4159	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2802	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ∪ cun 4152  {csn 4588  {cpr 4590  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4871

This theorem is used by:  unisn  4889  unisn3  4891  dfnfc2  4892  unisn2  5270  unisucs  6463  en2other2  10118  qustrivr  19429  pmtrprfv  19700  dprdsn  20285  indistopon  23352  ordtuni  23541  cmpcld  23753  ptcmplem5  24408  cldsubg  24463  icccmplem2  25176  vmappw  27476  chsupsn  32048  xrge0tsmseq  33712  cycpm2tr  33756  esumsnf  34779  prsiga  34846  rossros  34896  cvmscld  36218  unisnif  36878  topjoin  37344  fnejoin2  37348  bj-snmoore  38238  pibt2  38545  heiborlem8  38955  sucunisn  44576  onsucunitp  44578  oaun3  44587  fourierdlem80  47411