Theorem sneqd 3702

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

Syntax hints:   → wi 4   = wceq 1398  {csn 3689

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-sn 3695

This theorem is referenced by:  dmsnsnsng  5240  cnvsng  5248  ressn  5303  f1osng  5657  fsng  5850  fsn2g  5852  funopsn  5860  fnressn  5870  fvsng  5880  2nd1st  6374  dfmpo  6419  cnvf1olem  6420  suppsnopdc  6450  tpostpos  6495  tfrlemi1  6563  tfr1onlemaccex  6579  tfrcllemaccex  6592  elixpsn  6970  ixpsnf1o  6971  en1bg  7040  mapsnend  7052  mapsnen  7053  xpassen  7081  fztp  10412  fzsuc2  10413  fseq1p1m1  10428  fseq1m1p1  10429  zfz1isolemsplit  11210  zfz1isolem1  11212  s1val  11305  s1eq  11307  s1prc  11311  fsumm1  12102  fprodm1  12284  divalgmod  12613  ennnfonelemg  13154  ennnfonelemp1  13157  ennnfonelem1  13158  ennnfonelemnn0  13173  setsvalg  13242  strsetsid  13245  imasex  13518  imasival  13519  imasaddvallemg  13528  mulgval  13839  isunitd  14251  lspsnneg  14568  lspsnsub  14569  lmodindp1  14576  lidl0  14637  rsp0  14641  ridl0  14658  zrhrhmb  14770  znval  14784  psrval  14814  txdis  15142  upgr1een  16119  1loopgruspgr  16298  wkslem1  16315  wkslem2  16316  iswlk  16318  loopclwwlkn1b  16414  clwwlkn1loopb  16415  eupth2lem3lem3fi  16465