Metamath Proof Explorer

Theorem 2nalexn

Description: Part of theorem *11.5 in WhiteheadRussell p. 164. (Contributed by Andrew Salmon, 24-May-2011)

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

Proof

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