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

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

When possible, use of this theorem rather than ax9 1902 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 1644 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1530
This theorem is referenced by:  a9ev  1646  spimw  1656  equid  1662  sp  1728  spimeh  1734  equsalhw  1742  cbv3hv  1749  dvelimv  1892  ax10  1897  ax9  1902  cbv3hvNEW7  29423  dvelimvNEW7  29439  ax9NEW7  29445  ax10NEW7  29450  a12stdy1-x12  29733  ax10lem17ALT  29745  a12study10  29758  a12study10n  29759  ax9OLD  29781
This theorem was proved from axioms:  ax-9 1644
  Copyright terms: Public domain W3C validator