rmo5

Description: Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017)

		Ref	Expression
	Assertion	rmo5	$⊢ \exists^{*} x \in A φ \leftrightarrow (\exists x \in A φ \to \exists! x \in A φ)$

Step	Hyp	Ref	Expression
1		moeu	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow (\exists x (x \in A \land φ) \to \exists! x (x \in A \land φ))$
2		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
3		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
4		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
5	3 4	imbi12i	$⊢ (\exists x \in A φ \to \exists! x \in A φ) \leftrightarrow (\exists x (x \in A \land φ) \to \exists! x (x \in A \land φ))$
6	1 2 5	3bitr4i	$⊢ \exists^{*} x \in A φ \leftrightarrow (\exists x \in A φ \to \exists! x \in A φ)$

Metamath Proof Explorer