Theorem sneqd 3635

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

Syntax hints:   → wi 4   = wceq 1364  {csn 3622

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-sn 3628

This theorem is referenced by:  dmsnsnsng  5147  cnvsng  5155  ressn  5210  f1osng  5545  fsng  5735  fnressn  5748  fvsng  5758  2nd1st  6238  dfmpo  6281  cnvf1olem  6282  tpostpos  6322  tfrlemi1  6390  tfr1onlemaccex  6406  tfrcllemaccex  6419  elixpsn  6794  ixpsnf1o  6795  en1bg  6859  mapsnen  6870  xpassen  6889  fztp  10153  fzsuc2  10154  fseq1p1m1  10169  fseq1m1p1  10170  zfz1isolemsplit  10930  zfz1isolem1  10932  fsumm1  11581  fprodm1  11763  divalgmod  12092  ennnfonelemg  12620  ennnfonelemp1  12623  ennnfonelem1  12624  ennnfonelemnn0  12639  setsvalg  12708  strsetsid  12711  imasex  12948  imasival  12949  imasaddvallemg  12958  mulgval  13252  isunitd  13662  lspsnneg  13976  lspsnsub  13977  lmodindp1  13984  lidl0  14045  rsp0  14049  ridl0  14066  zrhrhmb  14178  znval  14192  psrval  14220  txdis  14513