 Existential quantifier introduction rule

From $A(t)$, infer $\exists xA(x)$ when the substitution is capture-free. The term $t$ supplies a witness.