Assignment Extension

Let there be a Variable Assignment $\phi$ into the Universe and $a\in \mathcal{D}$ then the extension of $\phi$ with $[a/X]$ (a for X) is defined as:

$\{(Y,a)\in \phi \mid Y\ne X\}\cup \{(X,a)\}:\phi ,[a/X]$ The extension coincides with $\phi$ off $X$, and gives $a$ there instead.