Theorem unisng 4876

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 4588	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4870	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4874	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4106	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2772	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∪ cun 3896  {csn 4575  {cpr 4577  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-sn 4576  df-pr 4578  df-uni 4859

This theorem is referenced by:  unisn  4877  unisn3  4879  dfnfc2  4880  unisn2  5252  unisucs  6390  en2other2  9907  pmtrprfv  19367  dprdsn  19952  indistopon  22917  ordtuni  23106  cmpcld  23318  ptcmplem5  23972  cldsubg  24027  icccmplem2  24740  vmappw  27054  chsupsn  31395  xrge0tsmseq  33051  cycpm2tr  33095  qustrivr  33337  esumsnf  34098  prsiga  34165  rossros  34214  cvmscld  35338  unisnif  35988  topjoin  36430  fnejoin2  36434  bj-snmoore  37178  pibt2  37482  heiborlem8  37879  sucunisn  43489  onsucunitp  43491  oaun3  43500  fourierdlem80  46309