# Metamath Proof Explorer

## Theorem moexex

Description: "At most one" double quantification. Usage of this theorem is discouraged because it depends on ax-13 . Use the version moexexvw when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 28-Dec-2018) Factor out common proof lines with moexexvw . (Revised by Wolf Lammen, 2-Oct-2023) (New usage is discouraged.)

Ref Expression
Hypothesis moexex.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion moexex ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 moexex.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 nfmo ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 nfe1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
4 3 nfmo ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
5 1 2 4 moexexlem ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$