Theorem sneqd 3722

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  {csn 3709

This proof depends on 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 proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3715

This theorem is used by:  dmsnsnsng  5265  cnvsng  5273  ressn  5328  f1osng  5682  fsng  5881  fsn2g  5883  funopsn  5891  fnressn  5901  fvsng  5911  2nd1st  6414  dfmpo  6459  cnvf1olem  6460  suppsnopdc  6490  tpostpos  6535  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  mapsnend  7099  mapsnen  7100  xpassen  7128  fztp  10495  fzsuc2  10496  fseq1p1m1  10511  fseq1m1p1  10512  zfz1isolemsplit  11304  zfz1isolem1  11306  s1val  11399  s1eq  11401  s1prc  11405  fsumm1  12199  fprodm1  12381  divalgmod  12710  ennnfonelemg  13343  ennnfonelemp1  13346  ennnfonelem1  13347  ennnfonelemnn0  13362  setsvalg  13431  strsetsid  13434  imasex  13675  imasival  13676  imasaddvallemg  13685  mulgval  13974  isunitd  14462  lspsnneg  14806  lspsnsub  14807  lmodindp1  14814  lidl0  14875  rsp0  14879  ridl0  14896  zrhrhmb  15006  znval  15020  psrval  15099  txdis  15427  upgr1een  16463  1loopgruspgr  16642  wkslem1  16659  wkslem2  16660  iswlk  16662  loopclwwlkn1b  16758  clwwlkn1loopb  16759  eupth2lem3lem3fi  16809  wexmiddifxylem  17143