Maps Defined by Cases

In the setting of Sets and Maps: Ordinary Notation: this lemma is a scheme, asserting one lemma for each property and pair of expressions as below, possibly with parameters. Let $A$ and $B$ be sets, let $P$ be a property of elements of $A$ expressed by a predicative formula, and let $t_{1}(x)$ and $t_{2}(x)$ be expressions built from defined set symbols such that, for every $x\in A$ with $P(x)$, the symbols in $t_{1}(x)$ are used properly and $t_{1}(x)\in B$, and, for every $x\in A$ without $P(x)$, the symbols in $t_{2}(x)$ are used properly and $t_{2}(x)\in B$.

¶ There is exactly one map $f:A\to B$ with $f(x)=t_{1}(x)$ for every $x\in A$ with $P(x)$, and $f(x)=t_{2}(x)$ for every $x\in A$ without $P(x)$.