Class existence theorem schema

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

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

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

Proof

#missing/proof

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

#state/develop | #lang/en | #SemBr