This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrexrmo

Description: Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017)

		Ref	Expression
	Assertion	nrexrmo	$⊢ \neg \exists x \in A φ \to \exists^{*} x \in A φ$

Step	Hyp	Ref	Expression
1		pm2.21	$⊢ \neg \exists x \in A φ \to (\exists x \in A φ \to \exists! x \in A φ)$
2		rmo5	$⊢ \exists^{*} x \in A φ \leftrightarrow (\exists x \in A φ \to \exists! x \in A φ)$
3	1 2	sylibr	$⊢ \neg \exists x \in A φ \to \exists^{*} x \in A φ$