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  5160  cnvsng  5168  ressn  5223  f1osng  5563  fsng  5753  funopsn  5762  fnressn  5770  fvsng  5780  2nd1st  6266  dfmpo  6309  cnvf1olem  6310  tpostpos  6350  tfrlemi1  6418  tfr1onlemaccex  6434  tfrcllemaccex  6447  elixpsn  6822  ixpsnf1o  6823  en1bg  6892  mapsnen  6903  xpassen  6925  fztp  10200  fzsuc2  10201  fseq1p1m1  10216  fseq1m1p1  10217  zfz1isolemsplit  10983  zfz1isolem1  10985  s1val  11071  s1eq  11073  s1prc  11077  fsumm1  11727  fprodm1  11909  divalgmod  12238  ennnfonelemg  12774  ennnfonelemp1  12777  ennnfonelem1  12778  ennnfonelemnn0  12793  setsvalg  12862  strsetsid  12865  imasex  13137  imasival  13138  imasaddvallemg  13147  mulgval  13458  isunitd  13868  lspsnneg  14182  lspsnsub  14183  lmodindp1  14190  lidl0  14251  rsp0  14255  ridl0  14272  zrhrhmb  14384  znval  14398  psrval  14428  txdis  14749