 Transfer: For each formula \(\phi(x)\) not mentioning the standardness predicate and containing no parameters (free variables other than \(x)\) except standard sets, \(\forall x\phi(x) \equiv \forall x\)(standard\((x) \rightarrow \phi(x))\).