Metamath Proof Explorer

Theorem alrmomodm

Description: Equivalence of an "at most one" and an "at most one" restricted to the domain inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	alrmomodm	$⊢ Rel R \to (\forall x \exists^{} u \in dom R u R x \leftrightarrow \forall x \exists^{} u u R x)$

Proof

Step	Hyp	Ref	Expression
1		df-rmo	$⊢ \exists^{} u \in dom R u R x \leftrightarrow \exists^{} u (u \in dom R \land u R x)$
2		brres	$⊢ x \in V \to (u ({R ↾}_{dom R}) x \leftrightarrow (u \in dom R \land u R x))$
3	2	elv	$⊢ u ({R ↾}_{dom R}) x \leftrightarrow (u \in dom R \land u R x)$
4		resdm	$⊢ Rel R \to {R ↾}_{dom R} = R$
5	4	breqd	$⊢ Rel R \to (u ({R ↾}_{dom R}) x \leftrightarrow u R x)$
6	3 5	bitr3id	$⊢ Rel R \to ((u \in dom R \land u R x) \leftrightarrow u R x)$
7	6	mobidv	$⊢ Rel R \to (\exists^{} u (u \in dom R \land u R x) \leftrightarrow \exists^{} u u R x)$
8	1 7	syl5bb	$⊢ Rel R \to (\exists^{} u \in dom R u R x \leftrightarrow \exists^{} u u R x)$
9	8	albidv	$⊢ Rel R \to (\forall x \exists^{} u \in dom R u R x \leftrightarrow \forall x \exists^{} u u R x)$