Inference rule 94: Existential introduction/generalization (declared)

Suppose that x is a variable which is freely substitutable for some variable y in the statement \phi . Given that the variable substitution [\phi | x \to y] holds, we may infer that the existence statement \exists x \phi holds: \cfrac{\vdash [\phi | x \to y]}{\vdash \exists x \phi}.