Theorem moanmo

Description: Nested at-most-one quantifiers. (Contributed by NM, 25-Jan-2006)

	Ref	Expression
Assertion	moanmo	$$⊢{\exists }^{*}x\left(\phi \wedge {\exists }^{*}x\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢{\exists }^{*}x\phi \to {\exists }^{*}x\phi$$
2		nfmo1	$$⊢Ⅎx{\exists }^{*}x\phi$$
3	2	moanim	$$⊢{\exists }^{*}x\left({\exists }^{*}x\phi \wedge \phi \right)\leftrightarrow \left({\exists }^{*}x\phi \to {\exists }^{*}x\phi \right)$$
4	1 3	mpbir	$$⊢{\exists }^{*}x\left({\exists }^{*}x\phi \wedge \phi \right)$$
5		ancom	$$⊢\left(\phi \wedge {\exists }^{*}x\phi \right)\leftrightarrow \left({\exists }^{*}x\phi \wedge \phi \right)$$
6	5	mobii	$$⊢{\exists }^{*}x\left(\phi \wedge {\exists }^{*}x\phi \right)\leftrightarrow {\exists }^{*}x\left({\exists }^{*}x\phi \wedge \phi \right)$$
7	4 6	mpbir	$$⊢{\exists }^{*}x\left(\phi \wedge {\exists }^{*}x\phi \right)$$