|Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms of predicate calculus with equality.
The antecedents imply as well as
, so must
be a different variable from both and
if the antecedents
hold. The axiom essentially states that if is neither nor
, then it is
irrelevant to the truth of .
The original version of this axiom was ax-12o 1664 ("o" for "old") and was
replaced with this shorter ax-12 1633 in December 2015. The old axiom is
proved from this one as theorem ax12o 1663. Conversely, this axiom is
proved from ax-12o 1664 as theorem ax12 1881.
Although this version is shorter, the original version ax-12o 1664 may be
more intuitive to understand, as well as more practical to work with,
because of the "distinctor" form of its antecedents.
This axiom can be weakened if desired by adding distinct variable
restrictions on pairs and .
To show that, we add
these restrictions to theorem ax12v 1634 use only ax12v 1634 for further
derivation. Thus ax12v 1634 should be the only theorem referencing this
axiom. Other theorems can reference either ax12v 1634 or ax12 1881.
(Contributed by NM, 21-Dec-2015.) (New usage is