Theorem dfdisjs

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

	Ref	Expression
Assertion	dfdisjs	$$⊢\mathrm{Disjs}=\left\{r\in \mathrm{Rels}|\wr r^{-1}\in \mathrm{CnvRefRels}\right\}$$

Proof

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