Metamath Proof Explorer

Theorem dfdisjALTV4

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV4 . (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	dfdisjALTV4	$⊢ Disj R \leftrightarrow (\forall x \exists^{*} u u R x \land Rel R)$

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