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 ∀x(x = y → φ) is a way of expressing "y substituted for x in wff φ". 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 ¬ ∀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 ¬ ∀xx = y a "distinctor".

Assertion

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

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 ∀x x = y
5	4	wn 1	. 2 wff ¬ ∀x x = y
6		wph	. . . 4 wff φ
7	3, 6	wi 2	. . . . 5 wff (x = y → φ)
8	7, 1	wal 672	. . . 4 wff ∀x(x = y → φ)
9	6, 8	wi 2	. . 3 wff (φ → ∀x(x = y → φ))
10	3, 9	wi 2	. 2 wff (x = y → (φ → ∀x(x = y → φ)))
11	5, 10	wi 2	1 wff (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))

This axiom is referenced by:  eqs2 829  ax11a 926

metamath.org