What does this notation mean $ x [ f / x ] \equiv _{df} f$?

Question

Its from the book Type Theory and Programming Languages, page 34 (pdf file page 47)(link). I understand the form $e[f/x]$ which (given the lambda ($(\lambda x.e) f$) means occurrences of x in e is replaced by f. But I don't understand the $ \equiv _{df} f$ part.

Answer 1

They are defining $e[f/x]$ inductively on the complexity of the expression $e$, first using simple cases where $e$ is just a variable.

The book is using $\equiv_{df}$ to mean "is defined to be."

So, first, $x[t/x]$ is always defined as $t$ and for any variable $y$, $y[t/x]$ is defined to be $y$. After defining for variables, they defe it for other lambda expressions.

Answer 2

The notation $ \equiv_{df} $ typically means that the two are defined to be equal.