Theorem unisn 4890

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592  df-uni 4872

This theorem is referenced by:  unisnv  4891  unidif0  5315  op1sta  6198  op2nda  6201  opswap  6202  fvssunirnOLD  6892  funfv  6948  dffv2  6956  nlim1  8453  tc2  9695  cflim2  10216  fin1a2lem12  10364  acsmapd  18513  ghmqusnsglem1  19212  ghmquskerlem1  19215  pmtrprfval  19417  lspuni0  20916  lss0v  20923  zrhval2  21418  indistopon  22888  refun0  23402  qtopeu  23603  hmphindis  23684  filconn  23770  ufildr  23818  cnextfres1  23955  bday1s  27743  old1  27787  madeoldsuc  27796  zs12bday  28343  dimval  33596  dimvalfi  33597  locfinref  33831  pstmfval  33886  esumval  34036  esumpfinval  34065  esumpfinvalf  34066  prsiga  34121  carsggect  34309  indispconn  35221  onsucsuccmpi  36431  bj-nuliotaALT  37046  heiborlem3  37807  isomenndlem  46528  uniimaelsetpreimafv  47397