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	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) ↔ ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		con34b	⊢ ( ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜑 ) ↔ ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 → ¬ ∃ 𝑦 ∃ 𝑥 𝜑 ) )
2		2nexaln	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )
3		2nexaln	⊢ ( ¬ ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 )
4	2 3	imbi12i	⊢ ( ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 → ¬ ∃ 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) )
5	1 4	bitr2i	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) ↔ ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜑 ) )