7.2.2 Existential introduction

If we see a proof of its existence, we can say that a property is true for some element:

n & A\{t/x\} \\
& \exists x A & I$\exists$\ n,t
\end{fitch*} \end{displaymath}

That $A\{ t/x\}$ is a substitution (maybe read ``$t$ over $x$'' and is done by changing $x$ to $t$).

This rule says that if we see $At$, where $t$ is any element, we can say that $\exists xAx$, because we know that when $x$ is $t$ then the formula is true.

Daniel Clemente Laboreo 2005-05-17