![]() |
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 2321. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2163 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1787 or df-bj-nnf 35218, directly or indirectly. (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-19.12 | ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modalbe 35182 | . 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑) | |
2 | excom 2163 | . . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑) | |
3 | axc7e 2312 | . . . 4 ⊢ (∃𝑦∀𝑦𝜑 → 𝜑) | |
4 | 3 | eximi 1838 | . . 3 ⊢ (∃𝑥∃𝑦∀𝑦𝜑 → ∃𝑥𝜑) |
5 | 2, 4 | sylbi 216 | . 2 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 → ∃𝑥𝜑) |
6 | 1, 5 | sylg 1826 | 1 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: bj-nnflemae 35258 bj-nnflemea 35259 |
Copyright terms: Public domain | W3C validator |