Class existence theorem schema

Let $𝜙 (𝑋 1, \dots, 𝑋 𝑛, 𝑌 1, \dots, 𝑌 𝑚)$ be a predicative formula. Then nbg

⊢ (\exists ℭ 𝔩 𝔰 𝑍) (\forall 𝔈 𝑥 1) \dots (\forall 𝔈 𝑥 𝑛) [(𝑥 1, \dots, 𝑥 𝑛) \in 𝑍 ⟺ 𝜑 (𝑥 1, \dots, 𝑥 𝑛, 𝑌 1, \dots, 𝑌 𝑚)]

for any classes $𝑌 1, \dots, 𝑌 𝑛$ .

Proof

proof

All of the Axioms of Class Existence are deductible from this theorem.