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

Metamath Proof Explorer

Theorem rmo0

Description: Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023)

Ref Expression
Assertion rmo0 ⊢ ∃* x ∈ ∅ φ

Proof

Step Hyp Ref Expression
1 rex0 ⊢ ¬ ∃ x ∈ ∅ φ
2 1 pm2.21i ⊢ ∃ x ∈ ∅ φ → ∃! x ∈ ∅ φ
3 rmo5 ⊢ ∃* x ∈ ∅ φ ↔ ∃ x ∈ ∅ φ → ∃! x ∈ ∅ φ
4 2 3 mpbir ⊢ ∃* x ∈ ∅ φ