Axiom ax-10 800

Description: Axiom of Quantifier Substitution. One of the 5 equality axioms of predicate calculus. This is a technical axiom wherein the antecedent is true only if x and y are the same variable, and in that case it doesn't matter which one you use in a quantifier. Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. (Strictly speaking, the antecedent is also true when x and y are different variables in the case of a one-element domain of discourse, but then the consequent is also true in a one-element domain. For compatibility with traditional predicate calculus all our predicate calculus axioms hold in a one-element domain, but this becomes unimportant in set theory where we show in dtru 1889 that at least 2 things exist.)

Assertion

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

Detailed syntax breakdown of Axiom ax-10

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

This axiom is referenced by:  eq4 821  eq5 824  del34 835  del35 836  sb6y 872  hbsb3 875  hbsb4 905  ddelimf2 907  hbeu 1016  nd1 3732  nd2 3733  axpowndlem3 3745

metamath.org