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

Metamath Proof Explorer

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 ⊢ Ⅎ x φ
Assertion moanim ⊢ ∃* x φ ∧ ψ ↔ φ → ∃* x ψ

Proof

Step Hyp Ref Expression
1 moanim.1 ⊢ Ⅎ x φ
2 ibar ⊢ φ → ψ ↔ φ ∧ ψ
3 1 2 mobid ⊢ φ → ∃* x ψ ↔ ∃* x φ ∧ ψ
4 simpl ⊢ φ ∧ ψ → φ
5 1 4 exlimi ⊢ ∃ x φ ∧ ψ → φ
6 3 5 moanimlem ⊢ ∃* x φ ∧ ψ ↔ φ → ∃* x ψ