Theorem unisng 4949

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 4661	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4943	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4947	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4180	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2784	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ∪ cun 3974  {csn 4648  {cpr 4650  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651  df-uni 4932

This theorem is referenced by:  unisn  4950  unisn3  4952  dfnfc2  4953  unisn2  5330  unisucs  6472  en2other2  10078  pmtrprfv  19495  dprdsn  20080  indistopon  23029  ordtuni  23219  cmpcld  23431  ptcmplem5  24085  cldsubg  24140  icccmplem2  24864  vmappw  27177  chsupsn  31445  xrge0tsmseq  33043  cycpm2tr  33112  qustrivr  33358  esumsnf  34028  prsiga  34095  rossros  34144  cvmscld  35241  unisnif  35889  topjoin  36331  fnejoin2  36335  bj-snmoore  37079  pibt2  37383  heiborlem8  37778  sucunisn  43333  onsucunitp  43335  oaun3  43344  fourierdlem80  46107