Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-spae | Structured version Visualization version Unicode version |
Description: Prove an instance of sp 2053 from
ax-13 2246 and Tarski's FOL only, without
distinct variable conditions. The antecedent
holds in a
multi-object universe only if is substituted for , or vice
versa, i.e. both variables are effectively the same. The converse
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 and can
help eliminating distinct variable conditions.
The antecedent 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 2047. Note that this theorem is also provable from ax-12 2047 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1897 and spaev 1978 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.) |
Ref | Expression |
---|---|
wl-spae |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aeveq 1982 | . . . . 5 | |
2 | 1 | adantl 482 | . . . 4 |
3 | 2 | a1d 25 | . . 3 |
4 | ax13v 2247 | . . . . . . 7 | |
5 | equtrr 1949 | . . . . . . . . 9 | |
6 | 5 | al2imi 1743 | . . . . . . . 8 |
7 | 6 | con3d 148 | . . . . . . 7 |
8 | 4, 7 | syl6 35 | . . . . . 6 |
9 | 8 | com13 88 | . . . . 5 |
10 | 9 | impcom 446 | . . . 4 |
11 | 10 | con4d 114 | . . 3 |
12 | 3, 11 | pm2.61dan 832 | . 2 |
13 | ax6evr 1942 | . 2 | |
14 | 12, 13 | exlimiiv 1859 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wa 384 wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |