Theorem unisn 4869

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {csn 4567  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  unisnv  4870  unidif0  5301  unidif0OLD  5302  op1sta  6189  op2nda  6192  opswap  6193  funfv  6927  dffv2  6935  nlim1  8424  tc2  9661  cflim2  10185  fin1a2lem12  10333  acsmapd  18520  ghmqusnsglem1  19255  ghmquskerlem1  19258  pmtrprfval  19462  lspuni0  21005  lss0v  21011  zrhval2  21488  indistopon  22966  refun0  23480  qtopeu  23681  hmphindis  23762  filconn  23848  ufildr  23896  cnextfres1  24033  bday1  27806  old1  27857  madeoldsuc  27877  dimval  33745  dimvalfi  33746  locfinref  33985  pstmfval  34040  esumval  34190  esumpfinval  34219  esumpfinvalf  34220  prsiga  34275  carsggect  34462  fineqvnttrclse  35268  indispconn  35416  onsucsuccmpi  36625  bj-nuliotaALT  37365  heiborlem3  38134  isomenndlem  46958  uniimaelsetpreimafv  47856