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

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

When possible, use of this theorem rather than ax9 1949 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 1662 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1546
This theorem is referenced by:  a9ev  1664  spimw  1676  equidOLD  1685  spOLD  1760  spimehOLD  1836  equsalhwOLD  1857  cbv3hvOLD  1875  dvelimvOLD  1994  ax10OLD  1998  ax9OLD  1999  cbv3hvNEW7  28800  dvelimvNEW7  28816  ax9NEW7  28822  ax10NEW7  28827
This theorem was proved from axioms:  ax-9 1662
  Copyright terms: Public domain W3C validator