Theorem sneqd 3718

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

Syntax hints:   → wi 4   = wceq 1402  {csn 3705

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3711

This theorem is referenced by:  dmsnsnsng  5260  cnvsng  5268  ressn  5323  f1osng  5677  fsng  5872  fsn2g  5874  funopsn  5882  fnressn  5892  fvsng  5902  2nd1st  6404  dfmpo  6449  cnvf1olem  6450  suppsnopdc  6480  tpostpos  6525  tfrlemi1  6593  tfr1onlemaccex  6609  tfrcllemaccex  6622  elixpsn  7007  ixpsnf1o  7008  en1bg  7077  mapsnend  7089  mapsnen  7090  xpassen  7118  fztp  10463  fzsuc2  10464  fseq1p1m1  10479  fseq1m1p1  10480  zfz1isolemsplit  11268  zfz1isolem1  11270  s1val  11363  s1eq  11365  s1prc  11369  fsumm1  12161  fprodm1  12343  divalgmod  12672  ennnfonelemg  13272  ennnfonelemp1  13275  ennnfonelem1  13276  ennnfonelemnn0  13291  setsvalg  13360  strsetsid  13363  imasex  13603  imasival  13604  imasaddvallemg  13613  mulgval  13902  isunitd  14386  lspsnneg  14729  lspsnsub  14730  lmodindp1  14737  lidl0  14798  rsp0  14802  ridl0  14819  zrhrhmb  14929  znval  14943  psrval  14973  txdis  15301  upgr1een  16279  1loopgruspgr  16458  wkslem1  16475  wkslem2  16476  iswlk  16478  loopclwwlkn1b  16574  clwwlkn1loopb  16575  eupth2lem3lem3fi  16625