|Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms for a non-logical predicate in our predicate calculus with
equality. Axiom scheme C14' in [Megill]
p. 448 (p. 16 of the preprint).
It is redundant if we include ax-17 1623; see theorem ax15 2054.
ax-17 1623 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-17 1623. We retain ax-15 2177 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-17 1623, which might be easier to study for some
This axiom is obsolete and should no longer be used. It is proved above
as theorem ax15 2054. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.)