Injectivity of a Map between Set Variables Is Predicative

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k<n$ be pairwise distinct.

(i) The condition "$x_{i}$ is an injective map $x_{i}:x_{j}\to x_{k}$" on $x_{0},\dots,x_{n-1}$ is expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables $x_{1},\dots,x_{N}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables.