Theorem sneqd 3620

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

Syntax hints:   → wi 4   = wceq 1364  {csn 3607

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-sn 3613

This theorem is referenced by:  dmsnsnsng  5124  cnvsng  5132  ressn  5187  f1osng  5521  fsng  5710  fnressn  5723  fvsng  5733  2nd1st  6205  dfmpo  6248  cnvf1olem  6249  tpostpos  6289  tfrlemi1  6357  tfr1onlemaccex  6373  tfrcllemaccex  6386  elixpsn  6761  ixpsnf1o  6762  en1bg  6826  mapsnen  6837  xpassen  6856  fztp  10108  fzsuc2  10109  fseq1p1m1  10124  fseq1m1p1  10125  zfz1isolemsplit  10850  zfz1isolem1  10852  fsumm1  11456  fprodm1  11638  divalgmod  11964  ennnfonelemg  12454  ennnfonelemp1  12457  ennnfonelem1  12458  ennnfonelemnn0  12473  setsvalg  12542  strsetsid  12545  imasex  12782  imasival  12783  imasaddvallemg  12792  mulgval  13064  isunitd  13456  lspsnneg  13736  lspsnsub  13737  lmodindp1  13744  lidl0  13805  rsp0  13809  ridl0  13825  zrhrhmb  13919  znval  13932  psrval  13944  txdis  14237