Membership induction theorem ($[\forall x((\forall y\in x\phi (y))\to \phi (x))]\to \forall x\phi (x)$)

Membership induction is the schema displayed, with set parameters permitted in $\phi$. The Axiom of foundation proves it by choosing a minimal counterexample in the transitive closure $\mathrm{TC}(\{x\})$ of the singleton containing a counterexample $x$. Conversely, if a nonempty set $a$ had no membership-minimal element, the property $x\notin a$ would be progressive, so induction would force $a$ to be empty. Thus over ZF without Axiom of foundation, this schema implies Axiom of foundation. It also implies that every set lies in the cumulative hierarchy: bound the stage indices of all members of a set by replacement, then place that set in the next power-set stage.