# Metamath Proof Explorer

## Theorem moanimv

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023)

Ref Expression
Assertion moanimv ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left({\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 ibar ${⊢}{\phi }\to \left({\psi }↔\left({\phi }\wedge {\psi }\right)\right)$
2 1 mobidv ${⊢}{\phi }\to \left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\right)$
3 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
4 3 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to {\phi }$
5 2 4 moanimlem ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left({\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$