Can a founded relation find minimal elements in proper classes? My definition of a founded relation $R$ on a (possibly proper) class $A$ is
$$R\mbox{ Fr }A\iff \forall x\subseteq A\,(x\neq\emptyset\rightarrow\exists y\in x\ \forall z\in x\ \neg zRy),$$
or equivalently,
$$R\mbox{ Fr }A\iff \forall x\subseteq A\,(x\neq\emptyset\rightarrow\exists y\in x\ x\cap R^{-1}\{y\}=\emptyset).$$
I am working in ZF, so obviously $x$ must be a set so that I can quantify over it. But I would like to conclude from this definition that 
$$X\subseteq A\rightarrow(X\neq\emptyset\rightarrow\exists y\in X\ \forall z\in X\ \neg zRy),$$
where $X$ is now an arbitrary class, which we can assume is a proper class. Since $X$ is then not included in the quantifier, I cannot immediately conclude this theorem, but my question is if it is possible for me to derive this by other means. If it is not true, are there definable counterexamples?
 A: $\newcommand{\rank}{\operatorname{rank}}$It can be proved using the notion of the rank of a set: $\rank(x)=\min\{\alpha\in\mathbf{ON}:x\in V_{\alpha+1}\}$, where the von Neumann hierarchy is defined by $V_0=0$, $V_{\alpha+1}=\wp(V_\alpha)$, and $V_\eta=\bigcup_{\xi<\eta}V_\xi$ if $\eta$ is a limit ordinal.
Suppose that $R$ is a foundational relation on $A$, and $\varnothing\ne X\subseteq A$. The idea is to show that if $X$ has no $R$-minimal element, there is a set $s\subseteq X$ that has no $R$-minimal element, contradicting the hypothesis that $R$ is foundational. We start by using the rank function to form a non-empty subset of $X$: let $$X_0=\left\{x\in X:\forall y\in X\big(\rank(x)\le\rank(y)\big)\right\}\;.$$ Note that $X_0\subseteq V_\alpha$ for some $\alpha$, so $X_0$ is a set. Now we want to expand $X_0$ to a set $s$ with the property that if $x\in s$ is not $R$-minimal in $X$, then $x$ is not $R$-minimal in $s$, either. We do this recursively: given a set $X_n$ for $n\in\omega$, we’d like to form $X_{n+1}$ by adding enough elements of $X$ to ensure that if $x\in X_n$ is not $R$-minimal in $X$, there is some $y\in X_{n+1}$ such that $yRx$. At the same time we want to be sure that $X_{n+1}$ is a set, so we use the minimal-rank trick again: let
$$X_{n+1}=X_n\cup\left\{x\in X:\exists y\in X_n\Big(xRy\land\forall z\in X\big(zRy\to\rank(x)\le\rank(z)\big)\Big)\right\}\;;$$
$X_{n+1}$ adds to $X_n$ the minimal-rank representatives of $\{x\in X:\exists y\in X_n(xRy)\}$, and since $X_{n+1}\subseteq X_n\cup V_\alpha$ for some $\alpha$, $X_{n+1}$ is a set.
By the replacement schema we can now form the set $s=\bigcup_{n\in\omega}X_n$. Clearly $0\ne s\subseteq X\subseteq A$. Let $x\in s$; $x\in X_n$ for some $n\in\omega$. If $x$ is not $R$-minimal in $X$, let $y\in X$ be of minimal rank such that $yRx$; then by construction $y\in X_{n+1}\subseteq s$.
Finally, suppose that $X$ has no $R$-minimal element. Then we’ve just shown that for each $x\in s$ there is a $y\in s$ such that $yRx$, i.e., that $s$ has no $R$-minimal element, contradiction the hypothesis that $R$ is foundational.
