|Description: Axiom of Distinct
Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-17 1400 to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory, but nonetheless it is technically necessary as you
can see from its uses.
This axiom is redundant if we include ax-17 1400; see theorem ax16 1676.
This axiom is obsolete and should no longer be used. It is proved above
as theorem ax16 1676. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.)