proving two statements are equivalent Let $X$ be a set, ler $R$ be a binary relation on $X$, let $PX$ be the set of subsets of $X$, then 1) and 2) are equivalent:
1) $\forall a\in X\ \forall A\in PX(\forall f\in X(aRf\rightarrow f\in A)\rightarrow\forall g\in X(aRg\rightarrow\forall h(gRh\rightarrow h\in A)))$
2)$\forall a,g,h((aRg,gRh)\rightarrow\forall A[(\forall f(aRf\rightarrow f\in A))\rightarrow h\in A])$
Is there a way to prove the equivalence?
 A: I think I have proven it without resorting to set-theoretic axioms. Let us introduce the following abbreviations:
$$\phi:= aRg, \psi:=gRh, \chi:={f\in A}, \mu:={h\in A}, \kappa:= aRf$$
The formulae now become (ignoring domain specifications):
$$\begin{align*}\forall a \forall A &\left((\forall f: \kappa \to \chi) \to \forall g[\phi\to\forall h(\psi\to\mu)]\right) \\ 
\forall a \forall g \forall h & \left((\phi \land \psi)\to\forall A[(\forall f:\kappa\to\chi)\to\mu]\right)\end{align*}$$
We will proceed by showing they are both equivalent to:
$$\forall a \forall A \forall g \forall h \, \left(\phi\land \psi \land (\forall f:\kappa\to\chi)\right) \to\mu$$
which basically follows from applying the rules:
$$\begin{align*}\phi \to \forall x \psi &\iff \forall x (\phi \to \psi) \\
\phi \to (\psi \to \chi) &\iff (\phi\land \psi)\to\chi\end{align*}$$
the first of which is valid whenever $x$ does not occur freely in $\phi$. Please let me know if you want this last part in more detail.
A: If you want a set-theoretic proof, one way is to prove that each is equivalent to the statement that $R$ is transitive:
$$\forall a,g,h\in X(aRg\land gRh\to aRh)\;.\tag{3}$$
For $a\in X$ let $R[a]=\{f\in X:aRf\}$. Then (1) can be rewritten as
$$\forall a\in X\forall A\in\wp(X)\Big(R[a]\subseteq A\to\forall g\in R[a](R[g]\subseteq A)\Big)\;,\tag{1'}$$
and (2) as
$$\forall a,g,h\in X\Big(aRg\land gRh\to\forall A\in\wp(X)(R[a]\subseteq A\to h\in A)\Big)\;,\tag{2'}$$
while transitivity becomes
$$\forall a,g,h\in X\Big(g\in R[a]\land h\in R[g]\to h\in R[a]\Big)\;.\tag{3'}$$
Now $\forall A\in\wp(X)(R[a]\subseteq A\to h\in A)$ is clearly equivalent to $h\in\bigcap\{A\in\wp(X):R[a]\subseteq A\}$, and that intersection is evidently just $R[a]$, so it’s easy to see that $(2')$ is equivalent to $(3')$.
$(1')$ clearly implies 
$$\forall a\in X\forall g\in R[a](R[g]\subseteq R[a])\;,\tag{1''}$$ which is easily seen to be equivalent to $(3')$. Finally, one can again use the fact that $R[a]=\bigcap\{A\in\wp(X):R[a]\subseteq A\}$ to show that $(1'')$ implies $(1')$.
