Theorem unisng 4885

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 4879	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4883	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 577	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4104	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2800	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∪ cun 3897  {csn 4584  {cpr 4586  ∪ cuni 4867

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  unisn  4886  unisn3  4888  dfnfc2  4889  unisn2  5266  unisucs  6435  en2other2  10069  qustrivr  19377  pmtrprfv  19647  dprdsn  20232  indistopon  23299  ordtuni  23488  cmpcld  23700  ptcmplem5  24355  cldsubg  24410  icccmplem2  25123  vmappw  27425  chsupsn  31997  xrge0tsmseq  33618  cycpm2tr  33662  esumsnf  34678  prsiga  34745  rossros  34795  cvmscld  36007  unisnif  36657  topjoin  37123  fnejoin2  37127  bj-snmoore  38002  pibt2  38308  heiborlem8  38720  sucunisn  44331  onsucunitp  44333  oaun3  44342  fourierdlem80  47140