La forma correcta de expresar el poder conjunto de axiomas es la primera frase que escribió:
$$\forall a\exists y\forall x(x \in y \iff \forall z(z \in x \rightarrow z \in a))$$
I. e., para cada conjunto $a$, hay un conjunto $y$ (el juego de poder de $a$), cuyos miembros son los subconjuntos de a $a$, es decir, los conjuntos de $x$, de tal manera que cada miembro de la $z$ $x$ es también un miembro de $a$.
Esto no es equivalente a la frase que usted describe como la "definición real" con la cuantificación $z$ se trasladó fuera de la bi-implicación. Que debe ser un error en sus notas, ya que dado cualquier conjunto $x$, se podría recoger $z \not\in x$ y el uso a la conclusión de que la $x$ es un miembro de el juego de poder de cualquier conjunto $a$.
Ver http://en.wikipedia.org/wiki/Prenex_normal_form de cómo mover los cuantificadores fuera de las conectivas proposicionales. Cuando pones $\phi \iff \psi$ en forma normal prenex, es necesario tratarla como $(\phi \Rightarrow \psi) \land (\psi \Rightarrow \phi)$ y el resultado va a ser un desastre para el poder establecido axioma ($z$ será universalmente cuantificado en un conjunto y existencialmente cuantificadas en el otro).
