eldisjs4

Description: Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	eldisjs4	$⊢ R \in Disjs \leftrightarrow (\forall x \exists^{*} u u R x \land R \in Rels)$

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

Metamath Proof Explorer