Things around $(\forall x)(\Psi \Rightarrow \Phi) \Leftrightarrow ((\exists z)\Psi) \Rightarrow \Phi)$

Question

Let $M,N$ be sets, $Q_M$ a set that depends on $M$ and $P(\cdot,\cdot)$ a property with two parameters (is it ok, to call these "parameters" or would "variables" have been better ?). Consider the following three statements:

i) $(\forall x\in M)(\forall y\in Q_M)[P(x,y)\Rightarrow x \in N]$

ii) $(\forall x\in M)[((\exists y\in Q_M)[P(x,y)])\Rightarrow x \in N]$

iii) $N=\{ x\in M \mid (\exists y\in Q_M)[P(x,y)]\}$

I would very much like to know the following:

1. I have been told that i) and ii) are equivalent, since they are an instance of a general scheme $$ (\forall x)(\Psi \Rightarrow \Phi) \Leftrightarrow ((\exists z)\Psi) \Rightarrow \Phi), $$ which holds if $z$ is not mentioned in $\Phi$, as Carl Mummert I think explained a long time ago - I can't find the entry right now.
   What are the "values" the $x,z,\Psi$ and $\Phi$ have to take, such that this scheme shows the equivalence of i) and ii) ?

2. What kind of setting do you need in which you can prove this general scheme ? Is it only predicate logic ? Or do you need ZFC to formalize this logic so you can you use set-theory to prove it ?

3. How to you prove it (or a corrected version of it, if the above is flawed; it seems to me that quantifiers are missing) ?

4. Is ii) equivalent to iii) ? How do you rigorously prove that ? Which ZFC axioms are needed for that proof ?

Answer 1

Hints:

1] Assuming that $x$ is not free in $\varphi$, here's a chain of equivalences:

(a) $\forall x(\psi(x) \to \varphi)$

(b) $\forall x(\neg\psi(x) \lor \varphi)$

(c) $\forall x\neg\psi(x) \lor \varphi$

(d) $\neg\forall x\neg\psi(x) \to \varphi$

(e) $\exists x\psi(x) \to \varphi$

The only step that might give you pause is the equivalence of (b) and (c): it might help to compare $(\neg\psi(a) \lor \varphi) \land (\neg\psi(b) \lor \varphi)$ and $(\neg\psi(a) \land \neg\psi(b)) \lor \varphi$. Note that equivalence of (a) and (e) is just a matter of first-order logic, and nothing to do with ZFC.

2] These are also equivalents:

(a') $(\forall x \in A)(\psi(x) \to \varphi)$

(b') $(\exists x \in A)\psi(x) \to \varphi$

by just the same kind of reasoning, and again just by appeal to first-order logic. You just need to unpack the abbreviations for restricted quantifiers.

3] To see your (i) implies (ii), instantiate (i) -- use a parameter to name an arbitrary object in $M$ -- apply an (a'/b')-type equivalence, and generalize to get (ii). You can then do the reverse equivalence.