A Term of One Type Whose Values Lie in a Class B Is a Term of Type B

This helper adopts the setting of Sets and Maps: Ordinary Notation; it is a statement of the metatheory about formulas and expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters and their values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard, with assignments satisfying $\gamma$ as in Conditions Expressed by a Predicative Formula, and Guards (iii); and let terms under $\gamma$ and their values be as in Terms and Typed Terms under a Guard (i), and terms of type $A$ under $\gamma$ as in Terms and Typed Terms under a Guard (ii).

(i) Let $A$ and $B$ be classes, and let $t$ be a term of type $A$ under $\gamma$ such that, under every assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, the value of $t$ lies in $B$. Then $t$ is a term of type $B$ under $\gamma$.