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\in A\to \neg \phi$$
Assertion	nrmo	$$⊢{\exists }^{*}x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		nrmo.1	$$⊢x\in A\to \neg \phi$$
2		mofal	$$⊢{\exists }^{*}x\perp$$
3	1	imori	$$⊢\left(\neg x\in A\vee \neg \phi \right)$$
4		ianor	$$⊢\neg \left(x\in A\wedge \phi \right)\leftrightarrow \left(\neg x\in A\vee \neg \phi \right)$$
5	3 4	mpbir	$$⊢\neg \left(x\in A\wedge \phi \right)$$
6	5	bifal	$$⊢\left(x\in A\wedge \phi \right)\leftrightarrow \perp$$
7	6	mobii	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)\leftrightarrow {\exists }^{*}x\perp$$
8	2 7	mpbir	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)$$
9		df-rmo	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \phi \right)$$
10	8 9	mpbir	$$⊢{\exists }^{*}x\in A\phi$$