Infer Menu:

Existential Instantiation Command

If you have a given of the form xP(x), then you can introduce a new variable into the proof to stand for a 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 variable you chose.

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, and that variable 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.