Theorem bj-alcomexcom

Description: Commutation of two existential quantifiers on a formula is equivalent to commutation of two universal quantifiers over the same variables on the negation of that formula. Can be placed in the ax-4 section, soon after 2nexaln , and used to prove excom . (Contributed by BJ, 29-Nov-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-alcomexcom	$$⊢\left(\forall x\forall y\neg \phi \to \forall y\forall x\neg \phi \right)\leftrightarrow \left(\exists y\exists x\phi \to \exists x\exists y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		con34b	$$⊢\left(\exists y\exists x\phi \to \exists x\exists y\phi \right)\leftrightarrow \left(\neg \exists x\exists y\phi \to \neg \exists y\exists x\phi \right)$$
2		2nexaln	$$⊢\neg \exists x\exists y\phi \leftrightarrow \forall x\forall y\neg \phi$$
3		2nexaln	$$⊢\neg \exists y\exists x\phi \leftrightarrow \forall y\forall x\neg \phi$$
4	2 3	imbi12i	$$⊢\left(\neg \exists x\exists y\phi \to \neg \exists y\exists x\phi \right)\leftrightarrow \left(\forall x\forall y\neg \phi \to \forall y\forall x\neg \phi \right)$$
5	1 4	bitr2i	$$⊢\left(\forall x\forall y\neg \phi \to \forall y\forall x\neg \phi \right)\leftrightarrow \left(\exists y\exists x\phi \to \exists x\exists y\phi \right)$$