ralrnmo

Description: On the range, "at most one" becomes "exactly one". (Contributed by Peter Mazsa, 27-Sep-2018) (Revised by Peter Mazsa, 2-Feb-2026)

		Ref	Expression
	Assertion	ralrnmo	$⊢ \forall x \in ran R \exists^{*} u u R x \leftrightarrow \forall x \in ran R \exists! u u R x$

Step	Hyp	Ref	Expression
1		dfrn2	$⊢ ran R = \{x \| \exists u u R x\}$
2	1	eqabri	$⊢ x \in ran R \leftrightarrow \exists u u R x$
3	2	biimpi	$⊢ x \in ran R \to \exists u u R x$
4	3	biantrurd	$⊢ x \in ran R \to (\exists^{} u u R x \leftrightarrow (\exists u u R x \land \exists^{} u u R x))$
5	4	ralbiia	$⊢ \forall x \in ran R \exists^{} u u R x \leftrightarrow \forall x \in ran R (\exists u u R x \land \exists^{} u u R x)$
6		df-eu	$⊢ \exists! u u R x \leftrightarrow (\exists u u R x \land \exists^{*} u u R x)$
7	6	ralbii	$⊢ \forall x \in ran R \exists! u u R x \leftrightarrow \forall x \in ran R (\exists u u R x \land \exists^{*} u u R x)$
8	5 7	bitr4i	$⊢ \forall x \in ran R \exists^{*} u u R x \leftrightarrow \forall x \in ran R \exists! u u R x$

Metamath Proof Explorer