From the wiki about lambda calculus, substitution section "Substitution, written E[V := R], is the process of replacing all free occurrences of the variable V in the expression E with expression R. Substitution on terms of the λ-calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any λ expression)."
Since y is a variable and not an expression why is the following substitution valid? y[x := N] ≡ y, if x ≠ y. Since there can be no "free x" in "y" as y is just a variable? I am pretty sure it is valid, but I don't understand it very well. Secondly why the condition x ≠ y ?