Existential elimination or Existential instantiation (∃E) is a basic rule of inference in first-order logic by which an existential statement is removed in a proof by applying introducing a new constant to represent its claim.
The existential elimination rule may be formally presented as follows:
∃xφ(x) 
φ(c)
… where c is a new constant.
The existential elimination rule simply states that, since we know that there exists something (at least one thing) for which φ is the case, we'll introduce a new constant to refer to that thing.