Axiom ax-16 922

Description: Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 925 below to be a metatheorem and not an axiom). Axiom scheme C16' 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. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 1889) but nonetheless technically necessary as you can see from its uses.

Assertion

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

Distinct variable group(s):   x,y

Detailed syntax breakdown of Axiom ax-16

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

This axiom is referenced by:  ax17eq 923  ax17el 924  ax11a 926  a16g 933  hbs1 986  hbsb 987  sbal1 996  exists2 1073  hbab 1096  alexeq 1409

metamath.org