Metamath Proof Explorer

Theorem inecmo3

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

		Ref	Expression
	Assertion	inecmo3	$⊢ (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land Rel R) \leftrightarrow (\forall x \exists^{*} u u R x \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		inecmo2	$⊢ (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land Rel R) \leftrightarrow (\forall x \exists^{*} u \in dom R u R x \land Rel R)$
2		alrmomodm	$⊢ Rel R \to (\forall x \exists^{} u \in dom R u R x \leftrightarrow \forall x \exists^{} u u R x)$
3	2	pm5.32ri	$⊢ (\forall x \exists^{} u \in dom R u R x \land Rel R) \leftrightarrow (\forall x \exists^{} u u R x \land Rel R)$
4	1 3	bitri	$⊢ (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land Rel R) \leftrightarrow (\forall x \exists^{*} u u R x \land Rel R)$