Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-19.12 Structured version   Visualization version   GIF version

Theorem bj-19.12 36147
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.)
Assertion
Ref Expression
bj-19.12 (∃𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)

Proof of Theorem bj-19.12
StepHypRef Expression
1 bj-modalbe 36074 . 2 (∃𝑥𝑦𝜑 → ∀𝑦𝑦𝑥𝑦𝜑)
2 excom 2154 . . 3 (∃𝑦𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝑦𝜑)
3 axc7e 2305 . . . 4 (∃𝑦𝑦𝜑𝜑)
43eximi 1829 . . 3 (∃𝑥𝑦𝑦𝜑 → ∃𝑥𝜑)
52, 4sylbi 216 . 2 (∃𝑦𝑥𝑦𝜑 → ∃𝑥𝜑)
61, 5sylg 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