Axiom ax-11 801

Description: Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The antecedent becomes false if the same variable is substituted for x and y, ensuring the axiom is sound whenever this is the case. The final consequent A.x(x = y -> ph) is a way of expressing "y substituted for x in wff ph". Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Axiom C8 of [Monk2] p. 105, from which it is easily proved by cases. To understand this easier, think of -. A.xx = y ->... as an informal equivalent for "if x and y are distinct variables then..." In some later theorems we call an antecedent of the form -. A.xx = y a "distinctor".

Assertion

Ref	Expression
ax-11	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

Detailed syntax breakdown of Axiom ax-11

Step	Hyp	Ref	Expression
1		vx	. . . . 5 set x
2		vy	. . . . 5 set y
3	1, 2	weq 797	. . . 4 wff x = y
4	3, 1	wal 672	. . 3 wff A.x x = y
5	4	wn 1	. 2 wff -. A.x x = y
6		wph	. . . 4 wff ph
7	3, 6	wi 2	. . . . 5 wff (x = y -> ph)
8	7, 1	wal 672	. . . 4 wff A.x(x = y -> ph)
9	6, 8	wi 2	. . 3 wff (ph -> A.x(x = y -> ph))
10	3, 9	wi 2	. 2 wff (x = y -> (ph -> A.x(x = y -> ph)))
11	5, 10	wi 2	1 wff (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

This axiom is referenced by:  eqs2 829  ax11a 926

metamath.org