Theorem ax6v 2003

Description: Axiom B7 of [Tarski] p. 75, which requires that 𝑥 and 𝑦 be distinct. This trivial proof is intended merely to weaken Axiom ax-6 2002 by adding a distinct variable restriction ($d). From here on, ax-6 2002 should not be referenced directly by any other proof, so that Theorem ax6 2416 will show that we can recover ax-6 2002 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 2003 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 2002.

When possible, use of this theorem rather than ax6 2416 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

Step	Hyp	Ref	Expression
1		ax-6 2002	1 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568

This proof depends on axioms:  ax-6 2002

This theorem is used by:  ax6ev  2004  spimw  2005  spimew  2006  iresn0n0  6064  bj-denot  37789  bj-axc10v  37920  axc5c4c711toc5  45647