Theorem wl-spae

Description: Prove an instance of sp from ax-13 and Tarski's FOL only, without distinct variable conditions. The antecedent A. x x = y holds in a multi-object universe only if y is substituted for x , or vice versa, i.e. both variables are effectively the same. The converse -. A. x x = y indicates that both variables are distinct, and it so provides a simple translation of a distinct variable condition to a logical term. In case studies A. x x = y and -. A. x x = y can help eliminating distinct variable conditions.

The antecedent A. x x = y is expressed in the theorem's name by the abbreviation ae standing for 'all equal'.

Note that we cannot provide a logical predicate telling us directly whether a logical expression contains a particular variable, as such a construct would usually contradict ax-12 .

Note that this theorem is also provable from ax-12 alone, so you can pick the axiom it is based on.

Compare this result to 19.3v and spaev having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021)

	Ref	Expression
Assertion	wl-spae	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		aeveq	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → 𝑥 = 𝑦 )
2	1	adantl	⊢ ( ( 𝑦 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑧 ) → 𝑥 = 𝑦 )
3	2	a1d	⊢ ( ( 𝑦 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
4		ax13v	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
5		equtrr	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) )
6	5	al2imi	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 𝑥 = 𝑧 ) )
7	6	con3d	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
8	4 7	syl6	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
9	8	com13	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
10	9	impcom	⊢ ( ( 𝑦 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ¬ 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
11	10	con4d	⊢ ( ( 𝑦 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
12	3 11	pm2.61dan	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
13		ax6evr	⊢ ∃ 𝑧 𝑦 = 𝑧
14	12 13	exlimiiv	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )