Theorem sneqd 3679

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

Syntax hints:   -> wi 4   = wceq 1395   {csn 3666

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-sn 3672

This theorem is referenced by:  dmsnsnsng  5209  cnvsng  5217  ressn  5272  f1osng  5619  fsng  5813  funopsn  5822  fnressn  5832  fvsng  5842  2nd1st  6335  dfmpo  6380  cnvf1olem  6381  tpostpos  6421  tfrlemi1  6489  tfr1onlemaccex  6505  tfrcllemaccex  6518  elixpsn  6895  ixpsnf1o  6896  en1bg  6965  mapsnen  6977  xpassen  7002  fztp  10291  fzsuc2  10292  fseq1p1m1  10307  fseq1m1p1  10308  zfz1isolemsplit  11078  zfz1isolem1  11080  s1val  11170  s1eq  11172  s1prc  11176  fsumm1  11948  fprodm1  12130  divalgmod  12459  ennnfonelemg  12995  ennnfonelemp1  12998  ennnfonelem1  12999  ennnfonelemnn0  13014  setsvalg  13083  strsetsid  13086  imasex  13359  imasival  13360  imasaddvallemg  13369  mulgval  13680  isunitd  14091  lspsnneg  14405  lspsnsub  14406  lmodindp1  14413  lidl0  14474  rsp0  14478  ridl0  14495  zrhrhmb  14607  znval  14621  psrval  14651  txdis  14972  wkslem1  16092  wkslem2  16093  iswlk  16095  loopclwwlkn1b  16187  clwwlkn1loopb  16188