Transformation rules 

Propositional calculus 
Rules of inference 
Rules of replacement 
Predicate logic 
In predicate logic, existential instantiation (also called existential elimination)^{[1]}^{[2]}^{[3]} is a rule of inference which says that, given a formula of the form , one may infer for a new constant symbol c. The rule has the restrictions that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof.
In one formal notation, the rule may be denoted by
where a is a new constant symbol that has not appeared in the proof.
YouTube Encyclopedic

1/3Views:1 9574395 808

Logic Lesson 18: Introducing Existential Instantiation and Generalization

Existential Instantiation Proof Example: Absolute Values

7. Logic Lecture: Predicate Logic: Formal Proofs of Validity: Existential Instantiation