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  10172  fzsuc2  10173  fseq1p1m1  10188  fseq1m1p1  10189  zfz1isolemsplit  10949  zfz1isolem1  10951  fsumm1  11600  fprodm1  11782  divalgmod  12111  ennnfonelemg  12647  ennnfonelemp1  12650  ennnfonelem1  12651  ennnfonelemnn0  12666  setsvalg  12735  strsetsid  12738  imasex  13009  imasival  13010  imasaddvallemg  13019  mulgval  13330  isunitd  13740  lspsnneg  14054  lspsnsub  14055  lmodindp1  14062  lidl0  14123  rsp0  14127  ridl0  14144  zrhrhmb  14256  znval  14270  psrval  14300  txdis  14621