![]() |
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 2314. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2154 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1778 or df-bj-nnf 36110, directly or indirectly. (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-19.12 | ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modalbe 36074 | . 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑) | |
2 | excom 2154 | . . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑) | |
3 | axc7e 2305 | . . . 4 ⊢ (∃𝑦∀𝑦𝜑 → 𝜑) | |
4 | 3 | eximi 1829 | . . 3 ⊢ (∃𝑥∃𝑦∀𝑦𝜑 → ∃𝑥𝜑) |
5 | 2, 4 | sylbi 216 | . 2 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 → ∃𝑥𝜑) |
6 | 1, 5 | sylg 1817 | 1 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-10 2129 ax-11 2146 ax-12 2163 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: bj-nnflemae 36150 bj-nnflemea 36151 |
Copyright terms: Public domain | W3C validator |