ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-16 GIF version

Axiom ax-16 1801
Description: Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 1513 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, but nonetheless it is technically necessary as you can see from its uses.

This axiom is redundant if we include ax-17 1513; see Theorem ax16 1800.

This axiom is obsolete and should no longer be used. It is proved above as Theorem ax16 1800. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

Assertion
Ref Expression
ax-16 (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-16
StepHypRef Expression
1 vx . . . 4 setvar 𝑥
2 vy . . . 4 setvar 𝑦
31, 2weq 1490 . . 3 wff 𝑥 = 𝑦
43, 1wal 1340 . 2 wff 𝑥 𝑥 = 𝑦
5 wph . . 3 wff 𝜑
65, 1wal 1340 . . 3 wff 𝑥𝜑
75, 6wi 4 . 2 wff (𝜑 → ∀𝑥𝜑)
84, 7wi 4 1 wff (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Colors of variables: wff set class
This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator