Theorem sneqd 3704

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sneqd	|- ( ph -> { A } = { B } )

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 |- ( ph -> A = B )
2		sneq 3702	. 2 |- ( A = B -> { A } = { B } )
3	1, 2	syl 14	1 |- ( ph -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1398   {csn 3691

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-sn 3697

This theorem is referenced by:  dmsnsnsng  5242  cnvsng  5250  ressn  5305  f1osng  5659  fsng  5852  fsn2g  5854  funopsn  5862  fnressn  5872  fvsng  5882  2nd1st  6376  dfmpo  6421  cnvf1olem  6422  suppsnopdc  6452  tpostpos  6497  tfrlemi1  6565  tfr1onlemaccex  6581  tfrcllemaccex  6594  elixpsn  6972  ixpsnf1o  6973  en1bg  7042  mapsnend  7054  mapsnen  7055  xpassen  7083  fztp  10419  fzsuc2  10420  fseq1p1m1  10435  fseq1m1p1  10436  zfz1isolemsplit  11218  zfz1isolem1  11220  s1val  11313  s1eq  11315  s1prc  11319  fsumm1  12110  fprodm1  12292  divalgmod  12621  ennnfonelemg  13175  ennnfonelemp1  13178  ennnfonelem1  13179  ennnfonelemnn0  13194  setsvalg  13263  strsetsid  13266  imasex  13539  imasival  13540  imasaddvallemg  13549  mulgval  13860  isunitd  14273  lspsnneg  14617  lspsnsub  14618  lmodindp1  14625  lidl0  14686  rsp0  14690  ridl0  14707  zrhrhmb  14819  znval  14833  psrval  14863  txdis  15191  upgr1een  16168  1loopgruspgr  16347  wkslem1  16364  wkslem2  16365  iswlk  16367  loopclwwlkn1b  16463  clwwlkn1loopb  16464  eupth2lem3lem3fi  16514