# Metamath Proof Explorer

## Theorem bj-alcomexcom

Description: Commutation of universal quantifiers implies commutation of existential quantifiers. 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}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 2nexaln ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
2 2nexaln ${⊢}¬\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
3 1 2 imbi12i ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to ¬\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
4 con4 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to ¬\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 3 4 sylbir ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$