![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > aev-o | Structured version Visualization version GIF version |
Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 34681. Version of aev 2134 using ax-c11 34676. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
aev-o | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbae-o 34692 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | |
2 | hbae-o 34692 | . . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑡∀𝑥 𝑥 = 𝑦) | |
3 | ax7 2098 | . . . . 5 ⊢ (𝑥 = 𝑡 → (𝑥 = 𝑦 → 𝑡 = 𝑦)) | |
4 | 3 | spimv 2402 | . . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑡 = 𝑦) |
5 | 2, 4 | alrimih 1900 | . . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑡 𝑡 = 𝑦) |
6 | ax7 2098 | . . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝑦 = 𝑡 → 𝑢 = 𝑡)) | |
7 | equcomi 2099 | . . . . . . . 8 ⊢ (𝑢 = 𝑡 → 𝑡 = 𝑢) | |
8 | 6, 7 | syl6 35 | . . . . . . 7 ⊢ (𝑦 = 𝑢 → (𝑦 = 𝑡 → 𝑡 = 𝑢)) |
9 | 8 | spimv 2402 | . . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑡 → 𝑡 = 𝑢) |
10 | 9 | aecoms-o 34691 | . . . . 5 ⊢ (∀𝑡 𝑡 = 𝑦 → 𝑡 = 𝑢) |
11 | 10 | axc4i-o 34687 | . . . 4 ⊢ (∀𝑡 𝑡 = 𝑦 → ∀𝑡 𝑡 = 𝑢) |
12 | hbae-o 34692 | . . . . 5 ⊢ (∀𝑡 𝑡 = 𝑢 → ∀𝑣∀𝑡 𝑡 = 𝑢) | |
13 | ax7 2098 | . . . . . 6 ⊢ (𝑡 = 𝑣 → (𝑡 = 𝑢 → 𝑣 = 𝑢)) | |
14 | 13 | spimv 2402 | . . . . 5 ⊢ (∀𝑡 𝑡 = 𝑢 → 𝑣 = 𝑢) |
15 | 12, 14 | alrimih 1900 | . . . 4 ⊢ (∀𝑡 𝑡 = 𝑢 → ∀𝑣 𝑣 = 𝑢) |
16 | aecom-o 34690 | . . . 4 ⊢ (∀𝑣 𝑣 = 𝑢 → ∀𝑢 𝑢 = 𝑣) | |
17 | 11, 15, 16 | 3syl 18 | . . 3 ⊢ (∀𝑡 𝑡 = 𝑦 → ∀𝑢 𝑢 = 𝑣) |
18 | ax7 2098 | . . . 4 ⊢ (𝑢 = 𝑤 → (𝑢 = 𝑣 → 𝑤 = 𝑣)) | |
19 | 18 | spimv 2402 | . . 3 ⊢ (∀𝑢 𝑢 = 𝑣 → 𝑤 = 𝑣) |
20 | 5, 17, 19 | 3syl 18 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑤 = 𝑣) |
21 | 1, 20 | alrimih 1900 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-11 2183 ax-12 2196 ax-13 2391 ax-c5 34672 ax-c4 34673 ax-c7 34674 ax-c10 34675 ax-c11 34676 ax-c9 34679 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 |
This theorem is referenced by: axc16g-o 34723 |
Copyright terms: Public domain | W3C validator |