 The variable \(x\) need not be free in \(A\), in which case \(A(t/x)\) is just \(A\). ‘E!’ may either be taken as primitive (in which case it requires no additional rules) or defined in terms of the identity predicate as in  Section 1.2.  For non-inclusive logic, we may add a rule that introduces \(\exists x\rE!x\).