Proof of Injectivity of a Map between Set Variables Is Predicative

Choose distinct set variables $p,u,u',v,v'$, none of them among $x_{0},\dots,x_{n-1}$. Since $i$, $j$ and $k$ are pairwise distinct, the variables $x_{i},x_{j},x_{k},p,u,u',v,v'$ are pairwise distinct, so Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (viii) apply with the set variables $x_{i}$, $x_{j}$ and $x_{k}$ as $F$, $A$ and $B$. Let

$$\psi=\mu(x_{i},x_{j},x_{k})\wedge\iota(x_{i}).$$

Both conjuncts are predicative by those clauses, hence so is $\psi$: a quantifier over a class variable in $\psi$ would lie in one of the conjuncts (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)). The free variables of $\psi$ are $x_{i}$, $x_{j}$ and $x_{k}$, all among $x_{0},\dots,x_{n-1}$, and $\psi$ has no parameters.

Fix an assignment of sets to $x_{0},\dots,x_{n-1}$. By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), $\mu(x_{i},x_{j},x_{k})$ holds if and only if $x_{i}$ is a map $x_{i}:x_{j}\to x_{k}$. If it is not, then $\psi$ fails and $x_{i}$ is not an injective map $x_{i}:x_{j}\to x_{k}$. If it is, then by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (viii), applied to the map $x_{i}:x_{j}\to x_{k}$, $\iota(x_{i})$ holds if and only if $x_{i}$ is injective. In both cases $\psi$ holds if and only if $x_{i}$ is an injective map $x_{i}:x_{j}\to x_{k}$, so $\psi$ expresses the condition, which proves (i).