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. sb62142).
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-c152200 and was replaced with this
shorter ax-121794 in Jan. 2007. The old axiom is proved from
this one as
theorem axc152045. Conversely, this axiom is proved from ax-c152200 as
theorem ax122214.

Juha Arpiainen proved the metalogical independence of this axiom (in the
form of the older axiom ax-c152200) from the others on 19-Jan-2006. See
item 9a at http://us.metamath.org/award2003.html.

See ax12v1795 and ax12v22043 for other equivalents of this axiom that
(unlike
this axiom) have distinct variable restrictions.

This axiom scheme is logically redundant (see ax12w1769) but is used as an
auxiliary axiom to achieve metalogical completeness. (Contributed by NM,
22-Jan-2007.)