 We first translate hybrid logic into first-order logic with equality. Given two new first-order variables \(\mathtt{a}\) and \(\mathtt{b}\), the translations \(\mathrm{ST}_\mathtt{a}\) and \(\mathrm{ST}_\mathtt{b}\) are defined by mutual recursion. We just give the translation \(\mathrm{ST}_\mathtt{a}\).