MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-16 Unicode version

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

This axiom is redundant if we include ax-17 1628; see theorem ax16 1925. Alternately, ax-17 1628 becomes logically redundant in the presence of this axiom, but without ax-17 1628 we lose the more powerful metalogic that results from being able to express the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). We retain ax-16 1926 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-17 1628, which might be easier to study for some theoretical purposes. (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-16  |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph ) )
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)

Detailed syntax breakdown of Axiom ax-16
StepHypRef Expression
1 vx . . . 4  set  x
2 vy . . . 4  set  y
31, 2weq 1620 . . 3  wff  x  =  y
43, 1wal 1532 . 2  wff  A. x  x  =  y
5 wph . . 3  wff  ph
65, 1wal 1532 . . 3  wff  A. x ph
75, 6wi 6 . 2  wff  ( ph  ->  A. x ph )
84, 7wi 6 1  wff  ( A. x  x  =  y  ->  ( ph  ->  A. x ph ) )
Colors of variables: wff set class
This axiom is referenced by:  ax17eq  1927  ax11v  1990  a16g  2000  a16g-o  2001  hbs1  2065  ax17el  2103  exists2  2203  ax10-16  26773
  Copyright terms: Public domain W3C validator