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. sb62182).
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-11o2225 ("o" for "old") and was
replaced with this shorter ax-111764 in Jan. 2007. The old axiom is
from this one as theorem ax11o2085. Conversely, this axiom is proved from
ax-11o2225 as theorem ax112239.