Theorem unisn 4891

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  Vcvv 3454  {csn 4588  ∪ cuni 4872

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4873

This theorem is used by:  unisnv  4892  unidif0  5328  unidif0OLD  5329  op1sta  6245  op2nda  6248  opswap  6249  funfv  7003  dffv2  7011  nlim1  8535  tc2  9778  fin1a2lem12  10528  acsmapd  18778  ghmqusnsglem1  19545  ghmquskerlem1  19548  pmtrprfval  19752  lspuni0  21336  lss0v  21342  zrhval2  21869  indistopon  23374  refun0  23889  qtopeu  24090  hmphindis  24171  filconn  24257  ufildr  24305  cnextfres1  24442  bday1  28257  old1  28308  madeoldsuc  28328  dimval  34344  dimvalfi  34345  locfinref  34584  pstmfval  34639  esumval  34789  esumpfinval  34818  esumpfinvalf  34819  prsiga  34874  carsggect  35061  fineqvnttrclse  35933  indispconn  36207  onsucsuccmpi  37446  bj-nuliotaALT  38243  heiborlem3  39013  isomenndlem  47813  uniimaelsetpreimafv  48751