Theorem unisn 4877

Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
unisn.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
unisn	⊢ ∪ {𝐴} = 𝐴

Proof of Theorem unisn

Step	Hyp	Ref	Expression
1		unisn.1	. 2 ⊢ 𝐴 ∈ V
2		unisng 4876	. 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3437  {csn 4575  ∪ cuni 4858

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-sn 4576  df-pr 4578  df-uni 4859

This theorem is referenced by:  unisnv  4878  unidif0  5300  op1sta  6177  op2nda  6180  opswap  6181  funfv  6915  dffv2  6923  nlim1  8410  tc2  9637  cflim2  10161  fin1a2lem12  10309  acsmapd  18462  ghmqusnsglem1  19194  ghmquskerlem1  19197  pmtrprfval  19401  lspuni0  20945  lss0v  20952  zrhval2  21447  indistopon  22917  refun0  23431  qtopeu  23632  hmphindis  23713  filconn  23799  ufildr  23847  cnextfres1  23984  bday1s  27776  old1  27821  madeoldsuc  27831  zs12bday  28395  dimval  33634  dimvalfi  33635  locfinref  33875  pstmfval  33930  esumval  34080  esumpfinval  34109  esumpfinvalf  34110  prsiga  34165  carsggect  34352  fineqvnttrclse  35165  indispconn  35299  onsucsuccmpi  36508  bj-nuliotaALT  37123  heiborlem3  37873  isomenndlem  46652  uniimaelsetpreimafv  47520