Tutorial 21: Existential Elimination
2013
Reading
Bergmann[2004] The Logic Book Section 10.1.
The Tutorial
Existential Elimination (often called 'Existential Instantiation') permits you to remove an existential quantifier from a formula which has an existential quantifier as its main connective. It is one of those rules which involves the adoption and dropping of an extra assumption (like ∼I,⊃I,∨E, and ≡I).
The circumstance that Existential Instantiation gets invoked looks like this.