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

Metamath Proof Explorer

Theorem mobii

Description: Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 17-Oct-2016)

Ref Expression
Hypothesis mobii.1 ⊢ ψ ↔ χ
Assertion mobii ⊢ ∃* x ψ ↔ ∃* x χ

Proof

Step Hyp Ref Expression
1 mobii.1 ⊢ ψ ↔ χ
2 mobi ⊢ ∀ x ψ ↔ χ → ∃* x ψ ↔ ∃* x χ
3 2 1 mpg ⊢ ∃* x ψ ↔ ∃* x χ