Existential instantiation

In predicate logic, existential instantiation (also called existential elimination) is a rule of inference which says that, given a formula of the form ( ∃ x ) ϕ ( x ) {\displaystyle (\exists x)\phi (x)} , one may infer ϕ ( c ) {\displaystyle \phi (c)} for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof.

Source: Wikipedia — Existential instantiation (CC BY-SA 4.0)