# Metamath Proof Explorer

## Theorem moaneu

Description: Nested at-most-one and unique existential quantifiers. (Contributed by NM, 25-Jan-2006) (Proof shortened by Wolf Lammen, 27-Dec-2018)

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

### Proof

Step Hyp Ref Expression
1 moanmo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 eumo ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 anim2i ${⊢}\left({\phi }\wedge \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left({\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
4 3 moimi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 1 4 ax-mp ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$