Theorem unisn 4893

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457  {csn 4591  ∪ cuni 4874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594  df-uni 4875

This theorem is used by:  unisnv  4894  unidif0  5332  unidif0OLD  5333  op1sta  6228  op2nda  6231  opswap  6232  funfv  6972  dffv2  6980  nlim1  8476  tc2  9712  cflim2  10258  fin1a2lem12  10406  acsmapd  18628  ghmqusnsglem1  19374  ghmquskerlem1  19377  pmtrprfval  19581  lspuni0  21161  lss0v  21167  zrhval2  21688  indistopon  23188  refun0  23703  qtopeu  23904  hmphindis  23985  filconn  24071  ufildr  24119  cnextfres1  24256  bday1  28038  old1  28089  madeoldsuc  28109  dimval  34031  dimvalfi  34032  locfinref  34271  pstmfval  34326  esumval  34476  esumpfinval  34505  esumpfinvalf  34506  prsiga  34561  carsggect  34749  fineqvnttrclse  35570  indispconn  35739  onsucsuccmpi  36987  bj-nuliotaALT  37727  heiborlem3  38497  isomenndlem  47277  uniimaelsetpreimafv  48178