eldisjs3

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

		Ref	Expression
	Assertion	eldisjs3	$⊢ R \in Disjs \leftrightarrow (\forall u \forall v \forall x ((u R x \land v R x) \to u = v) \land R \in Rels)$

Step	Hyp	Ref	Expression
1		eldisjs2	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \subseteq I \land R \in Rels)$
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 R \in Rels) \leftrightarrow (\forall u \forall v \forall x ((u R x \land v R x) \to u = v) \land R \in Rels)$
4	1 3	bitri	$⊢ R \in Disjs \leftrightarrow (\forall u \forall v \forall x ((u R x \land v R x) \to u = v) \land R \in Rels)$

Metamath Proof Explorer