Theorem moanim

Description: Introduction of a conjunct into "at most one" quantifier. For a version requiring disjoint variables, but fewer axioms, see moanimv . (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 24-Dec-2018)

	Ref	Expression
Hypothesis	moanim.1	⊢ Ⅎ 𝑥 𝜑
Assertion	moanim	⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		moanim.1	⊢ Ⅎ 𝑥 𝜑
2		ibar	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
3	1 2	mobid	⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
4		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
5	1 4	exlimi	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 )
6	3 5	moanimlem	⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 𝜓 ) )