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  funopsn  5829  fnressn  5839  fvsng  5849  2nd1st  6342  dfmpo  6387  cnvf1olem  6388  tpostpos  6429  tfrlemi1  6497  tfr1onlemaccex  6513  tfrcllemaccex  6526  elixpsn  6903  ixpsnf1o  6904  en1bg  6973  mapsnen  6985  xpassen  7013  fztp  10312  fzsuc2  10313  fseq1p1m1  10328  fseq1m1p1  10329  zfz1isolemsplit  11101  zfz1isolem1  11103  s1val  11193  s1eq  11195  s1prc  11199  fsumm1  11976  fprodm1  12158  divalgmod  12487  ennnfonelemg  13023  ennnfonelemp1  13026  ennnfonelem1  13027  ennnfonelemnn0  13042  setsvalg  13111  strsetsid  13114  imasex  13387  imasival  13388  imasaddvallemg  13397  mulgval  13708  isunitd  14119  lspsnneg  14433  lspsnsub  14434  lmodindp1  14441  lidl0  14502  rsp0  14506  ridl0  14523  zrhrhmb  14635  znval  14649  psrval  14679  txdis  15000  upgr1een  15974  1loopgruspgr  16153  wkslem1  16170  wkslem2  16171  iswlk  16173  loopclwwlkn1b  16269  clwwlkn1loopb  16270