Things around $(\forall x)(\Psi \Rightarrow \Phi) \Leftrightarrow ((\exists z)\Psi) \Rightarrow \Phi)$ 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:


*

*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) ?     

*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 ?       

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

*Is ii) equivalent to iii) ? How do you rigorously prove that ? Which ZFC axioms are needed for that proof ?
 A: 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.
