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  10485  fzsuc2  10486  fseq1p1m1  10501  fseq1m1p1  10502  zfz1isolemsplit  11290  zfz1isolem1  11292  s1val  11385  s1eq  11387  s1prc  11391  fsumm1  12183  fprodm1  12365  divalgmod  12694  ennnfonelemg  13294  ennnfonelemp1  13297  ennnfonelem1  13298  ennnfonelemnn0  13313  setsvalg  13382  strsetsid  13385  imasex  13626  imasival  13627  imasaddvallemg  13636  mulgval  13925  isunitd  14413  lspsnneg  14757  lspsnsub  14758  lmodindp1  14765  lidl0  14826  rsp0  14830  ridl0  14847  zrhrhmb  14957  znval  14971  psrval  15050  txdis  15378  upgr1een  16365  1loopgruspgr  16544  wkslem1  16561  wkslem2  16562  iswlk  16564  loopclwwlkn1b  16660  clwwlkn1loopb  16661  eupth2lem3lem3fi  16711  wexmiddifxylem  17045