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	|- ( ( A. x A. y -. ph -> A. y A. x -. ph ) <-> ( E. y E. x ph -> E. x E. y ph ) )

Proof

Step	Hyp	Ref	Expression
1		con34b	|- ( ( E. y E. x ph -> E. x E. y ph ) <-> ( -. E. x E. y ph -> -. E. y E. x ph ) )
2		2nexaln	|- ( -. E. x E. y ph <-> A. x A. y -. ph )
3		2nexaln	|- ( -. E. y E. x ph <-> A. y A. x -. ph )
4	2 3	imbi12i	|- ( ( -. E. x E. y ph -> -. E. y E. x ph ) <-> ( A. x A. y -. ph -> A. y A. x -. ph ) )
5	1 4	bitr2i	|- ( ( A. x A. y -. ph -> A. y A. x -. ph ) <-> ( E. y E. x ph -> E. x E. y ph ) )