Prenex form of the power set axiom I began teaching myself Zermelo-Fraenkel Set Theory today, and decided to test myself by writing down all the axioms I have read about without looking at the notes. On the axiom of power set, I wrote down:
$\forall a\exists y\forall x(x \in y \iff \forall z(z \in x \rightarrow z \in a))$
On looking at my notes, I see the actual definition is:
$\forall a\exists y\forall x\forall z(x \in y \iff (z \in x \rightarrow z \in a))$
My question is, was there any difference between what I wrote down and what is written in my notes? 
 A: The correct statement of the power set axiom is the first sentence you wrote down:
$$\forall a\exists y\forall x(x \in y \iff \forall z(z \in x \rightarrow z \in a))$$
I.e., for every set $a$, there is a set $y$ (the power set of $a$) whose members are the subsets of $a$, i.e., the sets $x$, such that every member $z$ of $x$ is also a member of $a$.
This is not equivalent to the sentence you describe as the "actual definition" with the quantification over $z$ moved outside the bi-implication. That must be an error in your notes, since given any set $x$, you could pick $z \not\in x$ and use it to conclude that $x$ is a member of the power set of any set $a$.
See http://en.wikipedia.org/wiki/Prenex_normal_form for how to move quantifiers outside the propositional connectives. When you put $\phi \iff \psi$ into prenex normal form, you need to treat it as $(\phi \Rightarrow \psi) \land (\psi \Rightarrow \phi)$ and the result will be a mess for the power set axiom ($z$ will be universally quantified in one conjunct and existentially quantified in the other).
