# Metamath Proof Explorer

## Theorem 19.12

Description: Theorem 19.12 of Margaris p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv and r19.12sn . (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 3-Jan-2018)

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

### Proof

Step Hyp Ref Expression
1 nfa1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 nfex ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 sp ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
4 3 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 2 4 alrimi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$