Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-spae | Structured version Visualization version GIF version |
Description: Prove an instance of sp 2182 from
ax-13 2390 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 2177. Note that this theorem is also provable from ax-12 2177 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1986 and spaev 2057 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 2061 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → 𝑥 = 𝑦) | |
2 | 1 | adantl 484 | . . . 4 ⊢ ((𝑦 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑧) → 𝑥 = 𝑦) |
3 | 2 | a1d 25 | . . 3 ⊢ ((𝑦 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
4 | ax13v 2391 | . . . . . . 7 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | |
5 | equtrr 2029 | . . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 → 𝑥 = 𝑧)) | |
6 | 5 | al2imi 1816 | . . . . . . . 8 ⊢ (∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑧)) |
7 | 6 | con3d 155 | . . . . . . 7 ⊢ (∀𝑥 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑥 = 𝑦)) |
8 | 4, 7 | syl6 35 | . . . . . 6 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑥 = 𝑦))) |
9 | 8 | com13 88 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦))) |
10 | 9 | impcom 410 | . . . 4 ⊢ ((𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)) |
11 | 10 | con4d 115 | . . 3 ⊢ ((𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
12 | 3, 11 | pm2.61dan 811 | . 2 ⊢ (𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
13 | ax6evr 2022 | . 2 ⊢ ∃𝑧 𝑦 = 𝑧 | |
14 | 12, 13 | exlimiiv 1932 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∀wal 1535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-13 2390 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |