Axiom ax-11 966

Description: Axiom of Variable 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 1266). 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, that isn't otherwise used in our development, was ax-11o 1217 ("o" for "old"), which was replaced with this shorter ax-11 966 in Jan. 2007.

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

Interestingly, if the wff expression substituted for φ contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-11o 1217 (from which the ax-11 966 instance follows by theorem ax11 1218.) The proof is by induction on formula length, using ax11eq 1362 and ax11el 1363 for the basis steps and ax11indn 1365, ax11indi 1366, and ax11inda 1370 for the induction steps.

See also ax11v 1264 and ax11v2 1214 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.

Assertion

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

Detailed syntax breakdown of Axiom ax-11

Step	Hyp	Ref	Expression
1		vx	. . . 4 set x
2	1	cv 954	. . 3 class x
3		vy	. . . 4 set y
4	3	cv 954	. . 3 class y
5	2, 4	wceq 955	. 2 wff x = y
6		wph	. . . 4 wff φ
7	6, 3	wal 953	. . 3 wff ∀yφ
8	5, 6	wi 3	. . . 4 wff (x = y → φ)
9	8, 1	wal 953	. . 3 wff ∀x(x = y → φ)
10	7, 9	wi 3	. 2 wff (∀yφ → ∀x(x = y → φ))
11	5, 10	wi 3	1 wff (x = y → (∀yφ → ∀x(x = y → φ)))

This axiom is referenced by:  ax4 971  ax10o 1138  equs5a 1196  equs5e 1197  ax11o 1216

Copyright terms: Public domain