Theorem unisng 4877

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 4589	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4871	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4875	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4107	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2770	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ∪ cun 3900  {csn 4576  {cpr 4578  ∪ cuni 4859

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-sn 4577  df-pr 4579  df-uni 4860

This theorem is referenced by:  unisn  4878  unisn3  4880  dfnfc2  4881  unisn2  5250  unisucs  6385  en2other2  9900  pmtrprfv  19366  dprdsn  19951  indistopon  22917  ordtuni  23106  cmpcld  23318  ptcmplem5  23972  cldsubg  24027  icccmplem2  24740  vmappw  27054  chsupsn  31391  xrge0tsmseq  33042  cycpm2tr  33086  qustrivr  33328  esumsnf  34075  prsiga  34142  rossros  34191  cvmscld  35315  unisnif  35965  topjoin  36405  fnejoin2  36409  bj-snmoore  37153  pibt2  37457  heiborlem8  37864  sucunisn  43410  onsucunitp  43412  oaun3  43421  fourierdlem80  46230