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

Metamath Proof Explorer

Theorem mormo

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

		Ref	Expression
	Assertion	mormo	$⊢ \exists^{} x φ \to \exists^{} x \in A φ$

Step	Hyp	Ref	Expression
1		moan	$⊢ \exists^{} x φ \to \exists^{} x (x \in A \land φ)$
2		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
3	1 2	sylibr	$⊢ \exists^{} x φ \to \exists^{} x \in A φ$