dfdisjALTV3

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV3 . (Contributed by Peter Mazsa, 28-Jul-2021)

		Ref	Expression
	Assertion	dfdisjALTV3	$⊢ Disj R \leftrightarrow (\forall u \forall v \forall x ((u R x \land v R x) \to u = v) \land Rel R)$

Step	Hyp	Ref	Expression
1		dfdisjALTV2	$⊢ Disj R \leftrightarrow (≀ R^{-1} \subseteq I \land Rel R)$
2		cosscnvssid3	$⊢ ≀ R^{-1} \subseteq I \leftrightarrow \forall u \forall v \forall x ((u R x \land v R x) \to u = v)$
3	2	anbi1i	$⊢ (≀ R^{-1} \subseteq I \land Rel R) \leftrightarrow (\forall u \forall v \forall x ((u R x \land v R x) \to u = v) \land Rel R)$
4	1 3	bitri	$⊢ Disj R \leftrightarrow (\forall u \forall v \forall x ((u R x \land v R x) \to u = v) \land Rel R)$

Metamath Proof Explorer