Theorem sneqd 3659

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

Syntax hints:   -> wi 4   = wceq 1375   {csn 3646

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-sn 3652

This theorem is referenced by:  dmsnsnsng  5182  cnvsng  5190  ressn  5245  f1osng  5590  fsng  5781  funopsn  5790  fnressn  5798  fvsng  5808  2nd1st  6296  dfmpo  6339  cnvf1olem  6340  tpostpos  6380  tfrlemi1  6448  tfr1onlemaccex  6464  tfrcllemaccex  6477  elixpsn  6852  ixpsnf1o  6853  en1bg  6922  mapsnen  6934  xpassen  6957  fztp  10242  fzsuc2  10243  fseq1p1m1  10258  fseq1m1p1  10259  zfz1isolemsplit  11027  zfz1isolem1  11029  s1val  11116  s1eq  11118  s1prc  11122  fsumm1  11893  fprodm1  12075  divalgmod  12404  ennnfonelemg  12940  ennnfonelemp1  12943  ennnfonelem1  12944  ennnfonelemnn0  12959  setsvalg  13028  strsetsid  13031  imasex  13304  imasival  13305  imasaddvallemg  13314  mulgval  13625  isunitd  14035  lspsnneg  14349  lspsnsub  14350  lmodindp1  14357  lidl0  14418  rsp0  14422  ridl0  14439  zrhrhmb  14551  znval  14565  psrval  14595  txdis  14916