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 | |- ( A. x x = y -> x = y ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aeveq | |- ( A. x x = z -> x = y ) |
|
2 | 1 | adantl | |- ( ( y = z /\ A. x x = z ) -> x = y ) |
3 | 2 | a1d | |- ( ( y = z /\ A. x x = z ) -> ( A. x x = y -> x = y ) ) |
4 | ax13v | |- ( -. x = y -> ( y = z -> A. x y = z ) ) |
|
5 | equtrr | |- ( y = z -> ( x = y -> x = z ) ) |
|
6 | 5 | al2imi | |- ( A. x y = z -> ( A. x x = y -> A. x x = z ) ) |
7 | 6 | con3d | |- ( A. x y = z -> ( -. A. x x = z -> -. A. x x = y ) ) |
8 | 4 7 | syl6 | |- ( -. x = y -> ( y = z -> ( -. A. x x = z -> -. A. x x = y ) ) ) |
9 | 8 | com13 | |- ( -. A. x x = z -> ( y = z -> ( -. x = y -> -. A. x x = y ) ) ) |
10 | 9 | impcom | |- ( ( y = z /\ -. A. x x = z ) -> ( -. x = y -> -. A. x x = y ) ) |
11 | 10 | con4d | |- ( ( y = z /\ -. A. x x = z ) -> ( A. x x = y -> x = y ) ) |
12 | 3 11 | pm2.61dan | |- ( y = z -> ( A. x x = y -> x = y ) ) |
13 | ax6evr | |- E. z y = z |
|
14 | 12 13 | exlimiiv | |- ( A. x x = y -> x = y ) |