**Description: **Axiom of Substitution.
One of the 5 equality axioms of predicate
calculus. The final consequent
is a way of
expressing "
substituted for in wff
" (cf. sb6 2182).
It
is based on Lemma 16 of [Tarski] p. 70 and
Axiom C8 of [Monk2] p. 105,
from which it can be proved by cases.
The original version of this axiom was ax-11o 2225 ("o" for "old") and was
replaced with this shorter ax-11 1764 in Jan. 2007. The old axiom is
proved
from this one as theorem ax11o 2085. Conversely, this axiom is proved from
ax-11o 2225 as theorem ax11 2239.
Juha Arpiainen proved the metalogical independence of this axiom (in the
form of the older axiom ax-11o 2225) from the others on 19-Jan-2006. See
item 9a at http://us.metamath.org/award2003.html.
See ax11v 2179 and ax11v2 2082 for other equivalents of this axiom that
(unlike
this axiom) have distinct variable restrictions.
This axiom scheme is logically redundant (see ax11w 1739) but is used as an
auxiliary axiom to achieve metalogical completeness. (Contributed by NM,
22-Jan-2007.) |