# ZF: Regularity axiom or axiom schema?

I have seen the axiom system ZF for set theory described including a single axiom of regularity (aka "foundation"), namely $$\forall x\neq\emptyset \, \exists y\in x \ y\cap x = \emptyset$$ and also including regularity as an infinite axiom schema, with an axiom for every formula $\varphi(x,x_1,..,x_n)$: $$\forall x_1,..,x_n \,\exists x \left(\varphi \rightarrow \exists x \, \left( \varphi \land \forall y\in x \ \neg \varphi\frac{y}{x}\right)\right)$$

The second version states that each non-empty class has an $\in$-minimal element, while the first one states that every non-empty set has an $\in$-minimal element. Is the second one stronger? Is it needed?

Let $\phi(x,x_1, \ldots, x_n)$ be a given formula. For given $x_1, \ldots, x_n$, suppose there is an $x$ such that $\phi(x, x_1, \ldots, x_n)$ holds. Let $X$ be the transitive closure of $\{x\}$ (which is a set) and
$z = \{y \in X \mid \phi(y, x_1, \ldots, x_n) \}$ Then $z$ is non-empty, by regularity, $z$ has an $\in$-minimal element $x'$. Let $y \in x'$, then $y \in X$ (as $X$ is transitive) and $y \not\in z$ (as $x'$ is $\in$-minimal), so $\neg\phi(y,x_1,\ldots, x_n)$. That is, $x'$ is an $\in$-minimal element of the class $\phi$.
So the schema follows from the other axioms of $\mathsf{ZF}$.