|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 2428). 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-c15 33651 and was replaced with this
shorter ax-12 2044 in Jan. 2007. The old axiom is proved from
this one as
theorem axc15 2302. Conversely, this axiom is proved from ax-c15 33651 as
theorem ax12 2303.
Juha Arpiainen proved the metalogical independence of this axiom (in the
form of the older axiom ax-c15 33651) from the others on 19-Jan-2006.
item 9a at http://us.metamath.org/award2003.html.
See ax12v 2045 and ax12v2 2046 for other equivalents of this axiom that
this axiom) have distinct variable restrictions.
This axiom scheme is logically redundant (see ax12w 2007) but is used as an
auxiliary axiom scheme to achieve scheme completeness. (Contributed by
NM, 22-Jan-2007.) (New usage is discouraged.)