Theorem ax6v

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-6 by adding a distinct variable restriction ($d). From here on, ax-6 should not be referenced directly by any other proof, so that Theorem ax6 will show that we can recover ax-6 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 prerequisite, similar to adding an unnecessary logical hypothesis, that results in a weakening of the theorem. This means that anyfuture theorem that references ax6v 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-6 .

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

	Ref	Expression
Assertion	ax6v	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦

Proof

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