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

Metamath Proof Explorer

Theorem nrmo

Description: "At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Hypothesis nrmo.1 ⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜑 )
Assertion nrmo ∃* 𝑥 ∈ 𝐴 𝜑

Proof

Step Hyp Ref Expression
1 nrmo.1 ⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜑 )
2 mofal ⊢ ∃* 𝑥 ⊥
3 1 imori ⊢ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝜑 )
4 ianor ⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝜑 ) )
5 3 4 mpbir ⊢ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
6 5 bifal ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ⊥ )
7 6 mobii ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃* 𝑥 ⊥ )
8 2 7 mpbir ⊢ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
9 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
10 8 9 mpbir ⊢ ∃* 𝑥 ∈ 𝐴 𝜑