Theorem sneqd 3679

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

Syntax hints:   → wi 4   = wceq 1395  {csn 3666

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-sn 3672

This theorem is referenced by:  dmsnsnsng  5205  cnvsng  5213  ressn  5268  f1osng  5613  fsng  5807  funopsn  5816  fnressn  5824  fvsng  5834  2nd1st  6324  dfmpo  6367  cnvf1olem  6368  tpostpos  6408  tfrlemi1  6476  tfr1onlemaccex  6492  tfrcllemaccex  6505  elixpsn  6880  ixpsnf1o  6881  en1bg  6950  mapsnen  6962  xpassen  6985  fztp  10270  fzsuc2  10271  fseq1p1m1  10286  fseq1m1p1  10287  zfz1isolemsplit  11055  zfz1isolem1  11057  s1val  11145  s1eq  11147  s1prc  11151  fsumm1  11922  fprodm1  12104  divalgmod  12433  ennnfonelemg  12969  ennnfonelemp1  12972  ennnfonelem1  12973  ennnfonelemnn0  12988  setsvalg  13057  strsetsid  13060  imasex  13333  imasival  13334  imasaddvallemg  13343  mulgval  13654  isunitd  14064  lspsnneg  14378  lspsnsub  14379  lmodindp1  14386  lidl0  14447  rsp0  14451  ridl0  14468  zrhrhmb  14580  znval  14594  psrval  14624  txdis  14945  wkslem1  16026  wkslem2  16027  iswlk  16029