The situation you are describing is not quantifier elimination but rather an application of function extensionality, the principles 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 princple of propositional extensionality which states $(P \Leftrightarrow Q) \Leftrightarrow P = Q$.

The situation you are describing is not quantifier elimination but rather an application of 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 which states $(P \Leftrightarrow Q) \Leftrightarrow P = Q$.