This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem moanimv

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023)

		Ref	Expression
	Assertion	moanimv	⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ibar	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
2	1	mobidv	⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
3		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
4	3	exlimiv	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 )
5	2 4	moanimlem	⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 𝜓 ) )