# Metamath Proof Explorer

## Theorem 2moexv

Description: Double quantification with "at most one". (Contributed by NM, 3-Dec-2001)

Ref Expression
Assertion 2moexv ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {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 nfe1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 nfmov ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 19.8a ${⊢}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 3 moimi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 2 4 alrimi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$