Theorem unisng 4863

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 4575	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4857	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4861	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 571	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4094	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2779	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ∪ cun 3888  {csn 4562  {cpr 4564  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565  df-uni 4846

This theorem is referenced by:  unisn  4864  unisn3  4866  dfnfc2  4867  unisn2  5241  unisucs  6396  en2other2  9929  pmtrprfv  19426  dprdsn  20011  indistopon  22991  ordtuni  23180  cmpcld  23392  ptcmplem5  24046  cldsubg  24101  icccmplem2  24814  vmappw  27104  chsupsn  31509  xrge0tsmseq  33163  cycpm2tr  33207  qustrivr  33455  esumsnf  34255  prsiga  34322  rossros  34371  cvmscld  35508  unisnif  36158  topjoin  36600  fnejoin2  36604  bj-snmoore  37478  pibt2  37786  heiborlem8  38192  sucunisn  43823  onsucunitp  43825  oaun3  43834  fourierdlem80  46636