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  10496  fzsuc2  10497  fseq1p1m1  10512  fseq1m1p1  10513  zfz1isolemsplit  11306  zfz1isolem1  11308  s1val  11401  s1eq  11403  s1prc  11407  fsumm1  12202  fprodm1  12384  divalgmod  12713  ennnfonelemg  13346  ennnfonelemp1  13349  ennnfonelem1  13350  ennnfonelemnn0  13365  setsvalg  13434  strsetsid  13437  imasex  13679  imasival  13680  imasaddvallemg  13689  mulgval  13978  isunitd  14497  lspsnneg  14841  lspsnsub  14842  lmodindp1  14849  lidl0  14910  rsp0  14914  ridl0  14931  zrhrhmb  15041  znval  15055  psrval  15134  txdis  15469  upgr1een  16531  1loopgruspgr  16710  wkslem1  16727  wkslem2  16728  iswlk  16730  loopclwwlkn1b  16826  clwwlkn1loopb  16827  eupth2lem3lem3fi  16877  wexmiddifxylem  17211