 Existential quantifier elimination rule

From $\exists xA(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.