Theorem unisng 4901

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 4614	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4895	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4899	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4132	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2774	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ∪ cun 3924  {csn 4601  {cpr 4603  ∪ cuni 4883

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-sn 4602  df-pr 4604  df-uni 4884

This theorem is referenced by:  unisn  4902  unisn3  4904  dfnfc2  4905  unisn2  5282  unisucs  6431  en2other2  10023  pmtrprfv  19434  dprdsn  20019  indistopon  22939  ordtuni  23128  cmpcld  23340  ptcmplem5  23994  cldsubg  24049  icccmplem2  24763  vmappw  27078  chsupsn  31394  xrge0tsmseq  33058  cycpm2tr  33130  qustrivr  33380  esumsnf  34095  prsiga  34162  rossros  34211  cvmscld  35295  unisnif  35943  topjoin  36383  fnejoin2  36387  bj-snmoore  37131  pibt2  37435  heiborlem8  37842  sucunisn  43395  onsucunitp  43397  oaun3  43406  fourierdlem80  46215