The complementary ∃Elim rule corresponds to giving a (new) name to a witness. Thus if you know "there exists some prime bigger than 5", then by ∃Elim we can think of giving some witness the name (say) c, and end up concluding "c is a prime bigger than 5". The caveats are that c must be a new name not already used in the proof, and different from any variables free in the conclusion we're aiming for. However, we will be able to use that variable c along with universal formulas to get useful statements.
Thus the general form of the rule is that . That is, we can rewrite the body of the exists, replacing the quantified variable p with any new variable name c, subject to the restrictions just mentioned.
- 817 reads