Theorem unisng 4891

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 4603	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4885	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4889	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 576	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4112	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2802	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ∪ cun 3904  {csn 4590  {cpr 4592  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593  df-uni 4874

This theorem is referenced by:  unisn  4892  unisn3  4894  dfnfc2  4895  unisn2  5276  unisucs  6442  en2other2  9994  qustrivr  19254  pmtrprfv  19524  dprdsn  20109  indistopon  23139  ordtuni  23328  cmpcld  23540  ptcmplem5  24194  cldsubg  24249  icccmplem2  24962  vmappw  27258  chsupsn  31743  xrge0tsmseq  33373  cycpm2tr  33417  esumsnf  34432  prsiga  34499  rossros  34548  cvmscld  35743  unisnif  36393  topjoin  36854  fnejoin2  36858  bj-snmoore  37733  pibt2  38041  heiborlem8  38447  sucunisn  44078  onsucunitp  44080  oaun3  44089  fourierdlem80  46880