This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfdisjs

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021)

		Ref	Expression
	Assertion	dfdisjs	$⊢ Disjs = \{r \in Rels \| ≀ r^{-1} \in CnvRefRels\}$

Step	Hyp	Ref	Expression
1		df-disjs	$⊢ Disjs = Disjss \cap Rels$
2		df-disjss	$⊢ Disjss = \{r \| ≀ r^{-1} \in CnvRefRels\}$
3	1 2	abeqin	$⊢ Disjs = \{r \in Rels \| ≀ r^{-1} \in CnvRefRels\}$