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

Theorem ax9v 1662
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 1661 by adding a distinct variable restriction. From here on, ax-9 1661 should not be referenced directly by any other proof, so that theorem ax9 1942 will show that we can recover ax-9 1661 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 1662 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 1661.

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

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

Proof of Theorem ax9v
StepHypRef Expression
1 ax-9 1661 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1546
This theorem is referenced by:  a9ev  1663  spimw  1675  equidOLD  1684  spOLD  1756  spimehOLD  1830  equsalhwOLD  1851  cbv3hvOLD  1863  a9e  1941  dvelimvOLD  1985  ax10OLD  1988  ax9OLD  1989  cbv3hvNEW7  28784  dvelimvNEW7  28800  ax9NEW7  28806  ax10NEW7  28811
This theorem was proved from axioms:  ax-9 1661
  Copyright terms: Public domain W3C validator