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 |
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 |