Theorem sneqd 3435

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

Syntax hints:   → wi 4   = wceq 1285  {csn 3422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-sn 3428

This theorem is referenced by:  dmsnsnsng  4862  cnvsng  4870  ressn  4925  f1osng  5242  fsng  5412  fnressn  5425  fvsng  5435  2nd1st  5885  dfmpt2  5923  cnvf1olem  5924  tpostpos  5961  tfrlemi1  6029  tfr1onlemaccex  6045  tfrcllemaccex  6058  en1bg  6447  mapsnen  6458  xpassen  6476  fztp  9385  fzsuc2  9386  fseq1p1m1  9401  fseq1m1p1  9402  divalgmod  10707