Transforming FOL sentences Can the implications (1a) and (1b) be derived from the equivalence (1)? 
$\forall x \forall y : (overlap(x,y) \equiv (\exists z : part(z,x) \land  part(z,y)))$                (1)
$\forall x \forall y : (overlap(x,y) \Rightarrow (\exists z : (part(z,x) \land  part(z,y)))) $            (1a)
$\forall x \forall y : ((\exists z : part(z,x) \land  part(z,y)) \Rightarrow overlap(x,y)) $                (1b)
Further, if I can prove (1b') does that count as a proof of (1b).
$\forall x \forall y \forall z  : ((part(z,x) \land  part(z,y)) \Rightarrow overlap(x,y)) $                   (1b')
In words, can I change the existentially quantified $z$ in  the antecedent of 1(b) to be universally quantified variable in (1b') and use a proof of (1b') as a proof of (1b)? 
 A: Yes and yes. Here are some general equivalence principles involving quantifiers you can use to show this:
Distribution $\forall$ over $\land$
$$\forall x (\phi(x) \land \psi(x)) \Leftrightarrow \forall x \ \phi(x) \land \forall x \psi(x)$$
Prenex Laws
Where $\varphi$ is any formula and where $x$ is not a free variable in $\psi$:
$$ \exists x \ \varphi \rightarrow \psi \Leftrightarrow \forall x (\varphi \rightarrow \psi)$$
Applied to your case:
$$\forall x \forall y : (overlap(x,y) \equiv (\exists z : part(z,x) \land  part(z,y))) \Leftrightarrow \text{ (Equivalence)}$$
$$\forall x \forall y : ((overlap(x,y) \rightarrow (\exists z : part(z,x) \land  part(z,y))) \land ((\exists z : part(z,x) \land  part(z,y))\rightarrow overlap(x,y))) \Leftrightarrow \text{ (Distribution } \forall \text{ over } \land \text{)}$$
$$\forall x(\forall y ((overlap(x,y) \rightarrow (\exists z : part(z,x) \land  part(z,y))) \land \forall y((\exists z : part(z,x) \land  part(z,y))\rightarrow overlap(x,y))) \Leftrightarrow \text{ (Distribution } \forall \text{ over } \land \text{)}$$
$$\forall x \forall y ((overlap(x,y) \rightarrow (\exists z : part(z,x) \land  part(z,y))) \land \forall y \forall y((\exists z : part(z,x) \land  part(z,y))\rightarrow overlap(x,y)))$$
So $(1)$ is equivalent to the conjunction of $(1a)$ and $(1b)$, meaning that the latter two can indeed be derived from the former.
And, once you have $(1b)$:
$$\forall y \forall y((\exists z : part(z,x) \land  part(z,y))\rightarrow overlap(x,y))) \Leftrightarrow \text{ (Prenex Law)}$$
$$\forall y \forall y \forall z((part(z,x) \land  part(z,y))\rightarrow overlap(x,y))) $$
So $(1b)$ is equivalent to $(1b')$, meaning that the latter logically follows from the former as well.
