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  5206  cnvsng  5214  ressn  5269  f1osng  5614  fsng  5808  funopsn  5817  fnressn  5825  fvsng  5835  2nd1st  6326  dfmpo  6369  cnvf1olem  6370  tpostpos  6410  tfrlemi1  6478  tfr1onlemaccex  6494  tfrcllemaccex  6507  elixpsn  6882  ixpsnf1o  6883  en1bg  6952  mapsnen  6964  xpassen  6989  fztp  10274  fzsuc2  10275  fseq1p1m1  10290  fseq1m1p1  10291  zfz1isolemsplit  11060  zfz1isolem1  11062  s1val  11150  s1eq  11152  s1prc  11156  fsumm1  11927  fprodm1  12109  divalgmod  12438  ennnfonelemg  12974  ennnfonelemp1  12977  ennnfonelem1  12978  ennnfonelemnn0  12993  setsvalg  13062  strsetsid  13065  imasex  13338  imasival  13339  imasaddvallemg  13348  mulgval  13659  isunitd  14070  lspsnneg  14384  lspsnsub  14385  lmodindp1  14392  lidl0  14453  rsp0  14457  ridl0  14474  zrhrhmb  14586  znval  14600  psrval  14630  txdis  14951  wkslem1  16033  wkslem2  16034  iswlk  16036