7.2.2 Enigo de ekzistokvantoro

Se oni vidas pruvon de ekzisto, oni rajtas diri ke iu propreco certas pro almenaŭ unu elemento:

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

Tio $A\{ t/x\}$ estas anstataŭigo (legata ``$t$ super $x$'', temas pri ŝanĝi $x$ al $t$).

Tiu regulo esprimas ke se oni vidas $At$, kie $t$ estas elemento, oni povas aserti ke $\exists xAx$, ĉar kiam $x$ estas $t$ ja certas la propreco.