Theorem bj-19.12

Description: See 19.12 . Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023) The proof should not rely on df-nf or df-bj-nnf , directly or indirectly. (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-19.12	$$⊢\exists x\forall y\phi \to \forall y\exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		bj-modalbe	$$⊢\exists x\forall y\phi \to \forall y\exists y\exists x\forall y\phi$$
2		excom	$$⊢\exists y\exists x\forall y\phi \leftrightarrow \exists x\exists y\forall y\phi$$
3		axc7e	$$⊢\exists y\forall y\phi \to \phi$$
4	3	eximi	$$⊢\exists x\exists y\forall y\phi \to \exists x\phi$$
5	2 4	sylbi	$$⊢\exists y\exists x\forall y\phi \to \exists x\phi$$
6	1 5	sylg	$$⊢\exists x\forall y\phi \to \forall y\exists x\phi$$