Frequent Links
Existential instantiation
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 valid rule of inference which says that, given a formula of the form <math>(\exists x) \phi(x)</math>, one may infer <math>\phi(c)</math> for a new constant or variable symbol c. The rule has the restriction that the constant or variable c introduced by the rule must be a new term that has not occurred earlier in the proof.
In one formal notation, the rule may be denoted
 <math>(\exists x)\mathcal{F}x :: \mathcal{F}a ,</math>
where a is an arbitrary term that has not been a part of our proof thus far.
See also
References
Lua error in package.lua at line 80: module 'Module:Buffer' not found.