Theorem sneqd 3686

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sneqd	⊢ (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sneq 3684	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1398  {csn 3673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-sn 3679

This theorem is referenced by:  dmsnsnsng  5221  cnvsng  5229  ressn  5284  f1osng  5635  fsng  5828  fsn2g  5830  funopsn  5838  fnressn  5848  fvsng  5858  2nd1st  6352  dfmpo  6397  cnvf1olem  6398  suppsnopdc  6428  tpostpos  6473  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  elixpsn  6947  ixpsnf1o  6948  en1bg  7017  mapsnen  7029  xpassen  7057  fztp  10358  fzsuc2  10359  fseq1p1m1  10374  fseq1m1p1  10375  zfz1isolemsplit  11148  zfz1isolem1  11150  s1val  11243  s1eq  11245  s1prc  11249  fsumm1  12040  fprodm1  12222  divalgmod  12551  ennnfonelemg  13087  ennnfonelemp1  13090  ennnfonelem1  13091  ennnfonelemnn0  13106  setsvalg  13175  strsetsid  13178  imasex  13451  imasival  13452  imasaddvallemg  13461  mulgval  13772  isunitd  14184  lspsnneg  14499  lspsnsub  14500  lmodindp1  14507  lidl0  14568  rsp0  14572  ridl0  14589  zrhrhmb  14701  znval  14715  psrval  14745  txdis  15071  upgr1een  16048  1loopgruspgr  16227  wkslem1  16244  wkslem2  16245  iswlk  16247  loopclwwlkn1b  16343  clwwlkn1loopb  16344  eupth2lem3lem3fi  16394