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

Metamath Proof Explorer

Theorem rmo2i

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

		Ref	Expression
	Hypothesis	rmo2.1	$⊢ Ⅎ y φ$
	Assertion	rmo2i	$⊢ \exists y \in A \forall x \in A (φ \to x = y) \to \exists^{*} x \in A φ$

Step	Hyp	Ref	Expression
1		rmo2.1	$⊢ Ⅎ y φ$
2		rexex	$⊢ \exists y \in A \forall x \in A (φ \to x = y) \to \exists y \forall x \in A (φ \to x = y)$
3	1	rmo2	$⊢ \exists^{*} x \in A φ \leftrightarrow \exists y \forall x \in A (φ \to x = y)$
4	2 3	sylibr	$⊢ \exists y \in A \forall x \in A (φ \to x = y) \to \exists^{*} x \in A φ$