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 x A ¬ φ
Assertion nrmo * x A φ

Proof

Step Hyp Ref Expression
1 nrmo.1 x A ¬ φ
2 mofal * x
3 1 imori ¬ x A ¬ φ
4 ianor ¬ x A φ ¬ x A ¬ φ
5 3 4 mpbir ¬ x A φ
6 5 bifal x A φ
7 6 mobii * x x A φ * x
8 2 7 mpbir * x x A φ
9 df-rmo * x A φ * x x A φ
10 8 9 mpbir * x A φ