Theorem sneqd 3651

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sneqd	⊢ (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sneq 3649	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1373  {csn 3638

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-sn 3644

This theorem is referenced by:  dmsnsnsng  5174  cnvsng  5182  ressn  5237  f1osng  5581  fsng  5771  funopsn  5780  fnressn  5788  fvsng  5798  2nd1st  6284  dfmpo  6327  cnvf1olem  6328  tpostpos  6368  tfrlemi1  6436  tfr1onlemaccex  6452  tfrcllemaccex  6465  elixpsn  6840  ixpsnf1o  6841  en1bg  6910  mapsnen  6922  xpassen  6945  fztp  10230  fzsuc2  10231  fseq1p1m1  10246  fseq1m1p1  10247  zfz1isolemsplit  11015  zfz1isolem1  11017  s1val  11104  s1eq  11106  s1prc  11110  fsumm1  11812  fprodm1  11994  divalgmod  12323  ennnfonelemg  12859  ennnfonelemp1  12862  ennnfonelem1  12863  ennnfonelemnn0  12878  setsvalg  12947  strsetsid  12950  imasex  13222  imasival  13223  imasaddvallemg  13232  mulgval  13543  isunitd  13953  lspsnneg  14267  lspsnsub  14268  lmodindp1  14275  lidl0  14336  rsp0  14340  ridl0  14357  zrhrhmb  14469  znval  14483  psrval  14513  txdis  14834