Can a property be generalized if always satisfied by the output of an axiom when its inputs satisfy it? Let $\phi(x)$ be a formula in the language of set theory with one free variable $x$, and let $\psi(x_1,\dots,x_n,y)$ be a formula with all free variables shown, and with $n>0$.
Let $T$ be the theory consisting of the following single axiom: $$\forall x_1\dots\forall x_n\, [\phi(x_1) \land \dots \land \phi(x_n) \rightarrow \exists y\, \psi(x_1,\dots,x_n,y)] $$
Now suppose that: $$T \vdash \forall x_1\dots\forall x_n \forall y\,  [\phi(x_1) \land \dots \land \phi(x_n) \land \psi(x_1,\dots,x_n,y) \rightarrow \phi(y)]$$
Is it always consistent to add the following sentence to $T$? $$ (\exists x \, \phi(x)) \rightarrow (\forall x\, \phi(x))$$
 A: For simplicity, I'll work in the language with one unary predicate $P$. To get counterexamples in the language of set theory, you can replace $P(x)$ with $x\in x$ (for example).
If you allow $n=0$, we get an easy counterexample. Let $\phi(x)$ be $P(x)\land \exists z\,\lnot P(z)$, and let $\psi(y)$ be $\phi(y)$. Then the axiom of $T$ reads $\exists y\,\phi(y)$, which is logically equivalent to $\exists y\, P(y)\land \exists z\,\lnot P(z)$. Modulo $T$, the sentence $\exists x\, \phi(x) \rightarrow \forall x\,\phi(x)$ implies $\forall x\,\phi(x)$, which entails $\forall x\, P(x)$ and thus is inconsistent with the axiom of $T$.

But you've specified $n>0$. Note that when $n>1$, both sentences under consideration are universal, so if we work in the version of first-order logic that allows empty models, they are consistent. So I assume that we work with "standard" first-order logic, in which there are no empty models and (for example) $\exists x\, x=x$ is a validity.
So take $n=1$, let $\phi(x)$ be $P(x)\rightarrow \forall y\, P(y)$, and let $\psi(x,y)$ be $x=x\land \lnot P(y)\land \exists z\,P(z)$.
Note that $\exists x\, \phi(x)$ is a validity - you may recognize it as the famous "drinker paradox". The axiom of $T$ is logically equivalent to $(\exists x\,\phi(x))\rightarrow (\exists y\,(\lnot P(y)\land \exists z\,P(z)))$, and hence is also logically equivalent to $(\exists y\,\lnot P(y))\land (\exists z\,P(z))$.
Your requirement on $T$ is satisfied: $T\vdash \forall x\forall y\, [\phi(x)\land \psi(x,y)\rightarrow \phi(y)]$, since $\psi(x,y)$ entails $\lnot P(y)$, which entails $\phi(y)$.
Now the sentence $\exists x\, \phi(x) \rightarrow \forall x\,\phi(x)$ is logically equivalent to $\forall x\, \phi(x)$. Unpacking, this is logically equivalent to $(\exists x\, P(x))\rightarrow (\forall y\, P(y))$, which contradicts the axiom of $T$.
