Theorem sneqd 3683

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 3681	. 2 |- ( A = B -> { A } = { B } )
3	1, 2	syl 14	1 |- ( ph -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1397   {csn 3670

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-sn 3676

This theorem is referenced by:  dmsnsnsng  5216  cnvsng  5224  ressn  5279  f1osng  5629  fsng  5823  fsn2g  5825  funopsn  5833  fnressn  5843  fvsng  5853  2nd1st  6348  dfmpo  6393  cnvf1olem  6394  tpostpos  6435  tfrlemi1  6503  tfr1onlemaccex  6519  tfrcllemaccex  6532  elixpsn  6909  ixpsnf1o  6910  en1bg  6979  mapsnen  6991  xpassen  7019  fztp  10318  fzsuc2  10319  fseq1p1m1  10334  fseq1m1p1  10335  zfz1isolemsplit  11108  zfz1isolem1  11110  s1val  11203  s1eq  11205  s1prc  11209  fsumm1  12000  fprodm1  12182  divalgmod  12511  ennnfonelemg  13047  ennnfonelemp1  13050  ennnfonelem1  13051  ennnfonelemnn0  13066  setsvalg  13135  strsetsid  13138  imasex  13411  imasival  13412  imasaddvallemg  13421  mulgval  13732  isunitd  14144  lspsnneg  14458  lspsnsub  14459  lmodindp1  14466  lidl0  14527  rsp0  14531  ridl0  14548  zrhrhmb  14660  znval  14674  psrval  14704  txdis  15030  upgr1een  16004  1loopgruspgr  16183  wkslem1  16200  wkslem2  16201  iswlk  16203  loopclwwlkn1b  16299  clwwlkn1loopb  16300  eupth2lem3lem3fi  16350