Theorem sneqd 3636

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

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

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 3629

This theorem is referenced by:  dmsnsnsng  5148  cnvsng  5156  ressn  5211  f1osng  5548  fsng  5738  fnressn  5751  fvsng  5761  2nd1st  6247  dfmpo  6290  cnvf1olem  6291  tpostpos  6331  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  elixpsn  6803  ixpsnf1o  6804  en1bg  6868  mapsnen  6879  xpassen  6898  fztp  10170  fzsuc2  10171  fseq1p1m1  10186  fseq1m1p1  10187  zfz1isolemsplit  10947  zfz1isolem1  10949  fsumm1  11598  fprodm1  11780  divalgmod  12109  ennnfonelemg  12645  ennnfonelemp1  12648  ennnfonelem1  12649  ennnfonelemnn0  12664  setsvalg  12733  strsetsid  12736  imasex  13007  imasival  13008  imasaddvallemg  13017  mulgval  13328  isunitd  13738  lspsnneg  14052  lspsnsub  14053  lmodindp1  14060  lidl0  14121  rsp0  14125  ridl0  14142  zrhrhmb  14254  znval  14268  psrval  14296  txdis  14597