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 e. A -> -. ph )
Assertion nrmo
|- E* x e. A ph

Proof

Step Hyp Ref Expression
1 nrmo.1
 |-  ( x e. A -> -. ph )
2 mofal
 |-  E* x F.
3 1 imori
 |-  ( -. x e. A \/ -. ph )
4 ianor
 |-  ( -. ( x e. A /\ ph ) <-> ( -. x e. A \/ -. ph ) )
5 3 4 mpbir
 |-  -. ( x e. A /\ ph )
6 5 bifal
 |-  ( ( x e. A /\ ph ) <-> F. )
7 6 mobii
 |-  ( E* x ( x e. A /\ ph ) <-> E* x F. )
8 2 7 mpbir
 |-  E* x ( x e. A /\ ph )
9 df-rmo
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
10 8 9 mpbir
 |-  E* x e. A ph