|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-5 1748; see theorem axc14 2166. Alternately,
ax-5 1748 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1748.
We retain ax-c14 32382 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1748, which might be easier to study for some
This axiom is obsolete and should no longer be used. It is proved above
as theorem axc14 2166. (Contributed by NM, 24-Jun-1993.)
(New usage is discouraged.)