Theorem unisn 4892

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4590  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593  df-uni 4874

This theorem is referenced by:  unisnv  4893  unidif0  5332  unidif0OLD  5333  op1sta  6228  op2nda  6231  opswap  6232  funfv  6970  dffv2  6978  nlim1  8475  tc2  9710  cflim2  10248  fin1a2lem12  10396  acsmapd  18611  ghmqusnsglem1  19351  ghmquskerlem1  19354  pmtrprfval  19558  lspuni0  21112  lss0v  21118  zrhval2  21639  indistopon  23139  refun0  23653  qtopeu  23854  hmphindis  23935  filconn  24021  ufildr  24069  cnextfres1  24206  bday1  27988  old1  28039  madeoldsuc  28059  dimval  33972  dimvalfi  33973  locfinref  34212  pstmfval  34267  esumval  34417  esumpfinval  34446  esumpfinvalf  34447  prsiga  34502  carsggect  34689  fineqvnttrclse  35518  indispconn  35707  onsucsuccmpi  36935  bj-nuliotaALT  37675  heiborlem3  38445  isomenndlem  47227  uniimaelsetpreimafv  48128