![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-19.12 | Structured version Visualization version GIF version |
Description: See 19.12 2326. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2160 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1781 or df-bj-nnf 36707, directly or indirectly. (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-19.12 | ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modalbe 36671 | . 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑) | |
2 | excom 2160 | . . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑) | |
3 | axc7e 2317 | . . . 4 ⊢ (∃𝑦∀𝑦𝜑 → 𝜑) | |
4 | 3 | eximi 1832 | . . 3 ⊢ (∃𝑥∃𝑦∀𝑦𝜑 → ∃𝑥𝜑) |
5 | 2, 4 | sylbi 217 | . 2 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 → ∃𝑥𝜑) |
6 | 1, 5 | sylg 1820 | 1 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-10 2139 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-ex 1777 |
This theorem is referenced by: bj-nnflemae 36747 bj-nnflemea 36748 |
Copyright terms: Public domain | W3C validator |