The Existence command can only be used when you
have a goal of the form 
xP(x). If you select a goal
of this form and give the Existence command, then a dialog box will
open, asking you what value should be substituted for x to make
P(x) true. If you know what value you want to use for
x, type it into the “Use this value” box and click OK. Proof
Designer will then say that you must prove P(x) for this
value of x in order to complete the proof.
If you don't know what value you want to use for x, you can use the “Use this new variable, whose definition will be inserted later” box. A default variable may be filled in already, but you can change it if you want to. You must choose a variable that is not already in use in the proof to stand for something else. If you choose this option, then Proof Designer will insert a new gap into the proof in which you must give a definition of the variable you chose, and then it will say that you must prove that P is true of the object named by that variable. Thus, there will now be two gaps in the proof: one for the definition of the new variable, and one for the proof that P is true for the value assigned to that variable. You can work on these two gaps in either order. In particular, you may find it useful to work on the proof that P is true until you reach the point where you know what value should be assigned to the variable, and then go back and fill in the definition of the variable. Hint: If, in the course of working on the proof that P is true, you decide to make an inference from some of the givens, you may want to make that inference in the first gap; after all, the inference may turn out to play a role in the definition of the variable, so you may want it to be available to be used in the gap in which that definition must be filled in.
If your goal starts with several existential quantifiers in a row, then you can handle as many of them as you want in one step. For each quantifier, you can choose to use either the “Use this value” box or the “Use this new variable” box. Make your choice for the first quantifier, and then click the Next button. Proof Designer will fill in the value or variable you selected and then ask what you want to do for the next quantifier. Once you have made your choice for the last quantifier you want to deal with, click OK.
The instructions above also apply if you have a goal of the form
x
AP(x), but in this case there is
also a shortcut you can use. If you have a goal of this
form, and you also have a given of
the form yA, then you may
select both and give the Existence command. No dialog box will open, and
Proof Designer will say that you must prove P(y) in order to
complete the proof.