Theorem sneqd 3707

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 3705	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

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

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-sn 3700

This theorem is referenced by:  dmsnsnsng  5245  cnvsng  5253  ressn  5308  f1osng  5662  fsng  5855  fsn2g  5857  funopsn  5865  fnressn  5875  fvsng  5885  2nd1st  6387  dfmpo  6432  cnvf1olem  6433  suppsnopdc  6463  tpostpos  6508  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  elixpsn  6983  ixpsnf1o  6984  en1bg  7053  mapsnend  7065  mapsnen  7066  xpassen  7094  fztp  10434  fzsuc2  10435  fseq1p1m1  10450  fseq1m1p1  10451  zfz1isolemsplit  11235  zfz1isolem1  11237  s1val  11330  s1eq  11332  s1prc  11336  fsumm1  12127  fprodm1  12309  divalgmod  12638  ennnfonelemg  13238  ennnfonelemp1  13241  ennnfonelem1  13242  ennnfonelemnn0  13257  setsvalg  13326  strsetsid  13329  imasex  13569  imasival  13570  imasaddvallemg  13579  mulgval  13875  isunitd  14351  lspsnneg  14694  lspsnsub  14695  lmodindp1  14702  lidl0  14763  rsp0  14767  ridl0  14784  zrhrhmb  14896  znval  14910  psrval  14940  txdis  15268  upgr1een  16245  1loopgruspgr  16424  wkslem1  16441  wkslem2  16442  iswlk  16444  loopclwwlkn1b  16540  clwwlkn1loopb  16541  eupth2lem3lem3fi  16591