Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-c16 Structured version   Visualization version   GIF version

Axiom ax-c16 34496
 Description: Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1879 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 4887), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1879; see theorem axc16 2173. Alternately, ax-5 1879 becomes logically redundant in the presence of this axiom, but without ax-5 1879 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 34496 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1879, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc16 2173. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
Assertion
Ref Expression
ax-c16 (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-c16
StepHypRef Expression
1 vx . . . 4 setvar 𝑥
2 vy . . . 4 setvar 𝑦
31, 2weq 1931 . . 3 wff 𝑥 = 𝑦
43, 1wal 1521 . 2 wff 𝑥 𝑥 = 𝑦
5 wph . . 3 wff 𝜑
65, 1wal 1521 . . 3 wff 𝑥𝜑
75, 6wi 4 . 2 wff (𝜑 → ∀𝑥𝜑)
84, 7wi 4 1 wff (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
 Colors of variables: wff setvar class This axiom is referenced by:  ax5eq  34536  axc16g-o  34538  ax5el  34541  axc11n-16  34542
 Copyright terms: Public domain W3C validator