Theorem sneqd 3682

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

Syntax hints:   → wi 4   = wceq 1397  {csn 3669

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-sn 3675

This theorem is referenced by:  dmsnsnsng  5214  cnvsng  5222  ressn  5277  f1osng  5626  fsng  5820  fsn2g  5822  funopsn  5830  fnressn  5840  fvsng  5850  2nd1st  6343  dfmpo  6388  cnvf1olem  6389  tpostpos  6430  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  elixpsn  6904  ixpsnf1o  6905  en1bg  6974  mapsnen  6986  xpassen  7014  fztp  10313  fzsuc2  10314  fseq1p1m1  10329  fseq1m1p1  10330  zfz1isolemsplit  11103  zfz1isolem1  11105  s1val  11198  s1eq  11200  s1prc  11204  fsumm1  11995  fprodm1  12177  divalgmod  12506  ennnfonelemg  13042  ennnfonelemp1  13045  ennnfonelem1  13046  ennnfonelemnn0  13061  setsvalg  13130  strsetsid  13133  imasex  13406  imasival  13407  imasaddvallemg  13416  mulgval  13727  isunitd  14139  lspsnneg  14453  lspsnsub  14454  lmodindp1  14461  lidl0  14522  rsp0  14526  ridl0  14543  zrhrhmb  14655  znval  14669  psrval  14699  txdis  15020  upgr1een  15994  1loopgruspgr  16173  wkslem1  16190  wkslem2  16191  iswlk  16193  loopclwwlkn1b  16289  clwwlkn1loopb  16290  eupth2lem3lem3fi  16340