## Goal Menu:

# Existence & Uniqueness Command

The Existence & Uniqueness command can only be used when you
have a goal of the form ∃!*x* *P*(*x*).
If you select a goal of
this form and give the Existence & Uniqueness command, then Proof
Designer will say that to complete the proof you have to prove both
∃*x* *P*(*x*) and
∀*x*∀*y*(*P*(*x*)∧*P*(*y*)→*x*=*y*).
The two parts of the proof are labeled Existence and Uniqueness.