Metamath Proof Explorer

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 ⊢ ∀ x x = y → x = y

Proof

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