|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 1626; see theorem ax15 2107.
ax-17 1626 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-17 1626. We retain ax-15 2220 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-17 1626, 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 2107. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.)