# Metamath Proof Explorer

## Theorem moimi

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006) Remove use of ax-5 . (Revised by Steven Nguyen, 9-May-2023)

Ref Expression
Hypothesis moimi.1 ${⊢}{\phi }\to {\psi }$
Assertion moimi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 moimi.1 ${⊢}{\phi }\to {\psi }$
2 1 imim1i ${⊢}\left({\psi }\to {x}={y}\right)\to \left({\phi }\to {x}={y}\right)$
3 2 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
4 3 eximi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
5 df-mo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)$
6 df-mo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
7 4 5 6 3imtr4i ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$