Theorem sneqd 3596

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 3594	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1348  {csn 3583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-sn 3589

This theorem is referenced by:  dmsnsnsng  5088  cnvsng  5096  ressn  5151  f1osng  5483  fsng  5669  fnressn  5682  fvsng  5692  2nd1st  6159  dfmpo  6202  cnvf1olem  6203  tpostpos  6243  tfrlemi1  6311  tfr1onlemaccex  6327  tfrcllemaccex  6340  elixpsn  6713  ixpsnf1o  6714  en1bg  6778  mapsnen  6789  xpassen  6808  fztp  10034  fzsuc2  10035  fseq1p1m1  10050  fseq1m1p1  10051  zfz1isolemsplit  10773  zfz1isolem1  10775  fsumm1  11379  fprodm1  11561  divalgmod  11886  ennnfonelemg  12358  ennnfonelemp1  12361  ennnfonelem1  12362  ennnfonelemnn0  12377  setsvalg  12446  strsetsid  12449  txdis  13071