 The use of the expression \(\eqdf\) which makes it appear that both flanking expressions are terms, disguises the fact that in this case of a “contextual definition” what occurs on each side  are formulas, the right hand side replacing the left hand side, thus “eliminating” the definite description.