The True Condition and Agreement of Two Classes at a Pair Are Predicative

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $x_{0},x_{1},\dots$ be distinct set variables. For a metatheoretic number $m\ge0$, a predicative formula in $x_{0},\dots,x_{m-1}$ is a predicative formula that expresses a condition on $x_{0},\dots,x_{m-1}$, with no displayed variables, as in Conditions Expressed by a Predicative Formula, and Guards (ii). There $x_{0},\dots,x_{m-1}$ take the place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i), whose parameters, fixed values and assignments are used throughout.

(i) For every metatheoretic number $n\ge0$, the condition on $x_{0},\dots,x_{n-1}$ that holds under every assignment is expressed by a predicative formula in $x_{0},\dots,x_{n-1}$.

(ii) Let $S$ and $M$ be class variables, parameters whose fixed values are classes, also denoted $S$ and $M$. Then the condition on $x_{0}$

$$\text{there is a set } v \text{ with } (x_{0},v)\in S \text{ and } (x_{0},v)\in M,$$

where $(x_{0},v)$ is the ordered pair and $v$ ranges over sets, is expressed by a predicative formula in $x_{0}$.