Theorem unisn 4878

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 4877	. 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4576  ∪ 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:  unisnv  4879  unidif0  5298  op1sta  6172  op2nda  6175  opswap  6176  funfv  6909  dffv2  6917  nlim1  8404  tc2  9632  cflim2  10151  fin1a2lem12  10299  acsmapd  18457  ghmqusnsglem1  19190  ghmquskerlem1  19193  pmtrprfval  19397  lspuni0  20941  lss0v  20948  zrhval2  21443  indistopon  22914  refun0  23428  qtopeu  23629  hmphindis  23710  filconn  23796  ufildr  23844  cnextfres1  23981  bday1s  27773  old1  27818  madeoldsuc  27828  zs12bday  28392  dimval  33608  dimvalfi  33609  locfinref  33849  pstmfval  33904  esumval  34054  esumpfinval  34083  esumpfinvalf  34084  prsiga  34139  carsggect  34326  fineqvnttrclse  35132  indispconn  35266  onsucsuccmpi  36476  bj-nuliotaALT  37091  heiborlem3  37852  isomenndlem  46567  uniimaelsetpreimafv  47426