MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax9v Structured version   Unicode version

Theorem ax9v 1668
Description: Axiom B7 of [Tarski] p. 75, which requires that  x and  y be distinct. This trivial proof is intended merely to weaken axiom ax-9 1667 by adding a distinct variable restriction. From here on, ax-9 1667 should not be referenced directly by any other proof, so that theorem ax9 1954 will show that we can recover ax-9 1667 from this weaker version if it were an axiom (as it is in the case of Tarski).

Note: Introducing  x ,  y as a distinct variable group "out of the blue" with no apparent justification has puzzled some people, but it is perfectly sound. All we are doing is adding an additional redundant requirement, no different from adding a redundant logical hypothesis, that results in a weakening of the theorem. This means that any future theorem that references ax9v 1668 must have a $d specified for the two variables that get substituted for  x and  y. The $d does not propagate "backwards" i.e. it does not impose a requirement on ax-9 1667.

When possible, use of this theorem rather than ax9 1954 is preferred since its derivation from axioms is much shorter. (Contributed by NM, 7-Aug-2015.)

Ref Expression
ax9v  |-  -.  A. x  -.  x  =  y
Distinct variable group:    x, y

Proof of Theorem ax9v
StepHypRef Expression
1 ax-9 1667 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1550
This theorem is referenced by:  a9ev  1669  spimw  1681  equidOLD  1690  spOLD  1765  spimehOLD  1841  equsalhwOLD  1862  cbv3hvOLD  1880  dvelimvOLD  2029  ax10OLD  2033  ax9OLD  2034  cbv3hvNEW7  29508  dvelimvNEW7  29524  ax9NEW7  29530  ax10NEW7  29535
This theorem was proved from axioms:  ax-9 1667
  Copyright terms: Public domain W3C validator