# Metamath Proof Explorer

## Theorem alexn

Description: A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993)

Ref Expression
Assertion alexn ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 exnal ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 albii ${⊢}\forall {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 }$
3 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 2 3 bitri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$