If you have a given of the form ∃*x* *P*(*x*)
or ∃!*x* *P*(*x*),
then you can introduce a new variable into the proof to stand for a value (or the unique value) of
*x* for which *P*(*x*)
is true. Select the given and give the Existential Instantiation command,
and a dialog box will open asking
what variable you would like to use to stand for the object that is
asserted to exist. You must choose a variable that is not already in use
in the proof to stand for something else. When you click OK, Proof
Designer will add a step to the proof asserting that *P* is true of
the object named by the variable you chose (and, if appropriate, that it is the only such object).

If the given starts with several existential quantifiers in a row, then you can introduce several new variables in one step. Choose a variable to stand for the first object asserted to exist, and then click the Next button. Proof Designer will fill in the variable you selected and then ask what name you would like to use for the next object. Once you have chosen a name for the last object you want to introduce, click OK.

If your goal is to define some variable *y*, and
*y* gets defined as a result of the Existential Instantiation
command, then Proof Designer will recognize that you have achieved your goal and remove the gap
from the proof. As a shortcut for this, you can select both an existential given statement
∃*x* *P*(*x*)
or ∃!*x* *P*(*x*) and the goal
*y*=?
and give the Existential Instantiation command. Proof Designer will use
*y* as the name of the object asserted to exist. Since this step
achieves the goal of defining *y*, Proof Designer will remove
the gap from the proof.