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. sb62125).
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-c152182 and was replaced with this
shorter ax-121785 in Jan. 2007. The old axiom is proved from
this one as
theorem axc152026. Conversely, this axiom is proved from ax-c152182 as