Axiom ax-11 1746

Description: Axiom of Substitution. One of the 5 equality axioms of predicate calculus. The final consequent ∀x(x = y → φ) is a way of expressing "y substituted for x in wff φ " (cf. sb6 2099). 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 2141 ("o" for "old") and was replaced with this shorter ax-11 1746 in Jan. 2007. The old axiom is proved from this one as Theorem ax11o 1994. Conversely, this axiom is proved from ax-11o 2141 as Theorem ax11 2155.

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

See ax11v 2096 and ax11v2 1992 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.

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

Assertion

Ref	Expression
ax-11	⊢ (x = y → (∀yφ → ∀x(x = y → φ)))

Detailed syntax breakdown of Axiom ax-11

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		vy	. . 3 setvar y
3	1, 2	weq 1643	. 2 wff x = y
4		wph	. . . 4 wff φ
5	4, 2	wal 1540	. . 3 wff ∀yφ
6	3, 4	wi 4	. . . 4 wff (x = y → φ)
7	6, 1	wal 1540	. . 3 wff ∀x(x = y → φ)
8	5, 7	wi 4	. 2 wff (∀yφ → ∀x(x = y → φ))
9	3, 8	wi 4	1 wff (x = y → (∀yφ → ∀x(x = y → φ)))

This axiom is referenced by:  sp  1747  spOLD  1748  equs5a  1887  equs5e  1888  dvelimv  1939  ax10lem6  1943  a16g  1945  ax10o  1952  ax11o  1994  ax11vALT  2097  axi11e  2332