Strategy Menu:

Existence & Uniqueness Command

The Existence & Uniqueness 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 & Uniqueness command, then Proof Designer will say that to complete the proof you have to prove both ∃xP(x) and ∀x∀y(P(x)∧P(y)→x = y). The two parts of the proof are labeled Existence and Uniqueness.