7.2.2 Existential introduction

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

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

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.