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

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

When possible, use of this theorem rather than ax9 1889 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 1635 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1527
This theorem is referenced by:  a9ev  1637  spimw  1638  equid  1644  sp  1716  spimeh  1722  equsalhw  1730  cbv3hv  1737  dvelimv  1879  ax10  1884  ax9  1889  a12stdy1-x12  29111  ax10lem17ALT  29123  a12study10  29136  a12study10n  29137  ax9OLD  29159
This theorem was proved from axioms:  ax-9 1635
  Copyright terms: Public domain W3C validator