MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax6v Structured version   Visualization version   GIF version

Theorem ax6v 1971
Description: Axiom B7 of [Tarski] p. 75, which requires that 𝑥 and 𝑦 be distinct. This trivial proof is intended merely to weaken axiom ax-6 1970 by adding a distinct variable restriction ($d). From here on, ax-6 1970 should not be referenced directly by any other proof, so that theorem ax6 2394 will show that we can recover ax-6 1970 from this weaker version if it were an axiom (as it is in the case of Tarski).

Note: Introducing 𝑥, 𝑦 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 prerequisite, similar to adding an unnecessary logical hypothesis, that results in a weakening of the theorem. This means that any future theorem that references ax6v 1971 must have a $d specified for the two variables that get substituted for 𝑥 and 𝑦. The $d does not propagate "backwards", i.e., it does not impose a requirement on ax-6 1970.

When possible, use of this theorem rather than ax6 2394 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 7-Aug-2015.)

Assertion
Ref Expression
ax6v ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem ax6v
StepHypRef Expression
1 ax-6 1970 1 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1536
This theorem was proved from axioms:  ax-6 1970
This theorem is referenced by:  ax6ev  1972  spimw  1973  spimew  1974  iresn0n0  5894  bj-denot  34121  bj-axc10v  34231  axc5c4c711toc5  41099
  Copyright terms: Public domain W3C validator