Existential introduction or Existential generalization (∃I) is a basic rule of inference in first-order logic by which an existential statement is introduced to a proof by generalizing a claim about a particular.
The existential introduction rule may be formally presented as follows:
φ(c) 
∃xφ(x)
… where c is any constant.
The existential elimination rule simply states that, if we know that a statement, φ, applies to any constant, we can more generally say that there exists something that is φ.