Theorem unisng 4884

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 4593	. . . 4 ⊢ {𝐴} = {𝐴, 𝐴}
2	1	unieqi 4878	. . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴}
3	2	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴})
4		uniprg 4882	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
5	4	anidms 577	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴))
6		unidm 4156	. . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴
7	6	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴)
8	3, 5, 7	3eqtrd 2799	1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ∪ cun 4149  {csn 4584  {cpr 4586  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587  df-uni 4867

This theorem is used by:  unisn  4885  unisn3  4887  dfnfc2  4888  unisn2  5265  unisucs  6442  en2other2  10091  qustrivr  19402  pmtrprfv  19672  dprdsn  20257  indistopon  23324  ordtuni  23513  cmpcld  23725  ptcmplem5  24380  cldsubg  24435  icccmplem2  25148  vmappw  27448  chsupsn  32020  xrge0tsmseq  33682  cycpm2tr  33726  esumsnf  34742  prsiga  34809  rossros  34859  cvmscld  36124  unisnif  36779  topjoin  37245  fnejoin2  37249  bj-snmoore  38126  pibt2  38433  heiborlem8  38845  sucunisn  44466  onsucunitp  44468  oaun3  44477  fourierdlem80  47289