moanmo

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

		Ref	Expression
	Assertion	moanmo	$⊢ \exists^{} x (φ \land \exists^{} x φ)$

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

Metamath Proof Explorer