$Mx =_{\beta\eta} Nx$ implies $M =_{\beta\eta} N$ In the context of $\lambda$-calculus, I was thinking about whether or not $$Mx =_{\beta\eta} Nx \implies M =_{\beta\eta} N$$ if $x\notin FV(M)\cup FV(N)$. I have been around this issue for quite some time now, but didn't reach anywhere useful.
Is it the case or not?
 A: This is true regardless of whether $x \in FV(MN)$.
Proof. By hypothesis:
$$Mx =_{\beta\eta} Nx \tag{1}$$ 
Then also:
$$(\lambda x.Mx) =_{\beta\eta} (\lambda x.Nx) \tag{2}$$
The justification for $(2)$ is that the sequence of (possibly partially reversed) $\beta\eta$-contractions that proves $(1)$ will also prove $(2)$ when applied to the subterm $Mx$ of $(\lambda x.Mx)$. 

As an aside, in the formal theory of $\lambda\beta\eta$ (and also $\lambda\beta$) this fact is accounted for by the 'weak extensionality' inference rule $\xi$:
\begin{align}
M &\;= M' \\
\hline 
(\lambda x.M) &\;= (\lambda x.M')
\tag{$\xi$}
\end{align}
Since 
$$ \lambda\beta\eta \vdash M = N \iff M =_{\beta\eta} N$$
you could in principle just cite rule $\xi$ to deduce $(2)$ from $(1)$.

Furthermore, by the $\eta$-rule:
$$(\lambda x.Mx) =_{\beta\eta} M \tag{3}$$
$$(\lambda x.Nx) =_{\beta\eta} N \tag{4}$$
So by $(2)$, $(3)$, $(4)$ and the symmetry and transitivity of $=_{\beta\eta}$ we have:
$$M =_{\beta\eta} (\lambda x.Mx) =_{\beta\eta} (\lambda x.Nx) =_{\beta\eta} N$$ 
which concludes the proof. $\square$
Note that the $\eta$-rule is generally added to a $\lambda$-theory to make it extensional (instead of intensional), so the truth of your statement was to be expected.
