Existential quantifier elimination rule
= Existential quantifier elimination rule
{title2=$\exists E$}
From $\exists x\,A(x)$, reason under a <temporary assumption> $A(u)$ for a fresh witness $u$. If this yields a conclusion $B$ not containing $u$ free, close the witness subproof and infer $B$. The <eigenvariable condition> also requires that $u$ not be free in other undischarged assumptions. The rule does not authorize selecting one fixed named object as a witness or allowing the witness to escape its scope.