ralmo

Description: "At most one" can be restricted to the range. (Contributed by Peter Mazsa, 2-Feb-2026)

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

Step	Hyp	Ref	Expression
1		brelrng	$⊢ (u \in V \land x \in V \land u R x) \to x \in ran R$
2	1	el3v12	$⊢ u R x \to x \in ran R$
3	2	pm4.71ri	$⊢ u R x \leftrightarrow (x \in ran R \land u R x)$
4	3	mobii	$⊢ \exists^{} u u R x \leftrightarrow \exists^{} u (x \in ran R \land u R x)$
5		moanimv	$⊢ \exists^{} u (x \in ran R \land u R x) \leftrightarrow (x \in ran R \to \exists^{} u u R x)$
6	4 5	bitri	$⊢ \exists^{} u u R x \leftrightarrow (x \in ran R \to \exists^{} u u R x)$
7	6	albii	$⊢ \forall x \exists^{} u u R x \leftrightarrow \forall x (x \in ran R \to \exists^{} u u R x)$
8		df-ral	$⊢ \forall x \in ran R \exists^{} u u R x \leftrightarrow \forall x (x \in ran R \to \exists^{} u u R x)$
9	7 8	bitr4i	$⊢ \forall x \exists^{} u u R x \leftrightarrow \forall x \in ran R \exists^{} u u R x$

Metamath Proof Explorer