| 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 2327. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2162 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1784 or df-bj-nnf 36725, directly or indirectly. (Proof modification is discouraged.) |
| Ref | Expression |
|---|---|
| bj-19.12 | ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-modalbe 36689 | . 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑) | |
| 2 | excom 2162 | . . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑) | |
| 3 | axc7e 2318 | . . . 4 ⊢ (∃𝑦∀𝑦𝜑 → 𝜑) | |
| 4 | 3 | eximi 1835 | . . 3 ⊢ (∃𝑥∃𝑦∀𝑦𝜑 → ∃𝑥𝜑) |
| 5 | 2, 4 | sylbi 217 | . 2 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 → ∃𝑥𝜑) |
| 6 | 1, 5 | sylg 1823 | 1 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: bj-nnflemae 36765 bj-nnflemea 36766 |
| Copyright terms: Public domain | W3C validator |