Theorem unisng 4892

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 4605	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4886	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4890	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 566	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4123	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2769	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∪ cun 3915  {csn 4592  {cpr 4594  ∪ cuni 4874

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-sn 4593  df-pr 4595  df-uni 4875

This theorem is referenced by:  unisn  4893  unisn3  4895  dfnfc2  4896  unisn2  5270  unisucs  6414  en2other2  9969  pmtrprfv  19390  dprdsn  19975  indistopon  22895  ordtuni  23084  cmpcld  23296  ptcmplem5  23950  cldsubg  24005  icccmplem2  24719  vmappw  27033  chsupsn  31349  xrge0tsmseq  33011  cycpm2tr  33083  qustrivr  33343  esumsnf  34061  prsiga  34128  rossros  34177  cvmscld  35267  unisnif  35920  topjoin  36360  fnejoin2  36364  bj-snmoore  37108  pibt2  37412  heiborlem8  37819  sucunisn  43367  onsucunitp  43369  oaun3  43378  fourierdlem80  46191