Theorem sneqd 3535

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

Syntax hints:   → wi 4   = wceq 1331  {csn 3522

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-sn 3528

This theorem is referenced by:  dmsnsnsng  5011  cnvsng  5019  ressn  5074  f1osng  5401  fsng  5586  fnressn  5599  fvsng  5609  2nd1st  6071  dfmpo  6113  cnvf1olem  6114  tpostpos  6154  tfrlemi1  6222  tfr1onlemaccex  6238  tfrcllemaccex  6251  elixpsn  6622  ixpsnf1o  6623  en1bg  6687  mapsnen  6698  xpassen  6717  fztp  9851  fzsuc2  9852  fseq1p1m1  9867  fseq1m1p1  9868  zfz1isolemsplit  10574  zfz1isolem1  10576  fsumm1  11178  divalgmod  11613  ennnfonelemg  11905  ennnfonelemp1  11908  ennnfonelem1  11909  ennnfonelemnn0  11924  setsvalg  11978  strsetsid  11981  txdis  12435