Theorem moanmo

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

	Ref	Expression
Assertion	moanmo	⊢ ∃* 𝑥 ( 𝜑 ∧ ∃* 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ∃* 𝑥 𝜑 → ∃* 𝑥 𝜑 )
2		nfmo1	⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
3	2	moanim	⊢ ( ∃* 𝑥 ( ∃* 𝑥 𝜑 ∧ 𝜑 ) ↔ ( ∃* 𝑥 𝜑 → ∃* 𝑥 𝜑 ) )
4	1 3	mpbir	⊢ ∃* 𝑥 ( ∃* 𝑥 𝜑 ∧ 𝜑 )
5		ancom	⊢ ( ( 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃* 𝑥 𝜑 ∧ 𝜑 ) )
6	5	mobii	⊢ ( ∃* 𝑥 ( 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ∃* 𝑥 ( ∃* 𝑥 𝜑 ∧ 𝜑 ) )
7	4 6	mpbir	⊢ ∃* 𝑥 ( 𝜑 ∧ ∃* 𝑥 𝜑 )