The situation you are describing is not quantifier elimination but rather an application of **[function extensionality](https://ncatlab.org/nlab/show/function+extensionality)**, the principle stating that, for any functions $f, g$ with domain $A$,
$$(\forall x \in A.\, f(x) = g(x)) \Leftrightarrow f = g.$$
Since you are also using $\Leftrightarrow$ in one place where $=$ might be expected, let me just point out that there is also the principle of [propositional extensionality](https://ncatlab.org/nlab/show/propositional+extensionality) which states $(P \Leftrightarrow Q) \Leftrightarrow P = Q$.