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

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

Metamath Proof Explorer