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