Rule of existential generalization, similar to universal generalization [ax-gen], but valid only if an individual exists. Its proof requires [ax-6] in our axiomatization but the equality predicate does not occur in its statement. Some fundamental theorems of predicate calculus can be proven from [ax-gen], [ax-4] and this theorem alone, not requiring [ax-7] or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.) (Proof shortened by Wolf Lammen, 20-Oct-2023.)