Theorem sneqd 3646

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

Syntax hints:   -> wi 4   = wceq 1373   {csn 3633

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-sn 3639

This theorem is referenced by:  dmsnsnsng  5161  cnvsng  5169  ressn  5224  f1osng  5565  fsng  5755  funopsn  5764  fnressn  5772  fvsng  5782  2nd1st  6268  dfmpo  6311  cnvf1olem  6312  tpostpos  6352  tfrlemi1  6420  tfr1onlemaccex  6436  tfrcllemaccex  6449  elixpsn  6824  ixpsnf1o  6825  en1bg  6894  mapsnen  6905  xpassen  6927  fztp  10202  fzsuc2  10203  fseq1p1m1  10218  fseq1m1p1  10219  zfz1isolemsplit  10985  zfz1isolem1  10987  s1val  11074  s1eq  11076  s1prc  11080  fsumm1  11760  fprodm1  11942  divalgmod  12271  ennnfonelemg  12807  ennnfonelemp1  12810  ennnfonelem1  12811  ennnfonelemnn0  12826  setsvalg  12895  strsetsid  12898  imasex  13170  imasival  13171  imasaddvallemg  13180  mulgval  13491  isunitd  13901  lspsnneg  14215  lspsnsub  14216  lmodindp1  14223  lidl0  14284  rsp0  14288  ridl0  14305  zrhrhmb  14417  znval  14431  psrval  14461  txdis  14782