Definition df-disjss

Description: Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs ). It is used only by df-disjs . (Contributed by Peter Mazsa, 17-Jul-2021)

	Ref	Expression
Assertion	df-disjss	$$⊢\mathrm{Disjss}=\left\{x|\wr x^{-1}\in \mathrm{CnvRefRels}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdisjss	$$class\mathrm{Disjss}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3	2	ccnv	$$class{x}^{-1}$$
4	3	ccoss	$$class\wr x^{-1}$$
5		ccnvrefrels	$$class\mathrm{CnvRefRels}$$
6	4 5	wcel	$$wff\wr x^{-1}\in \mathrm{CnvRefRels}$$
7	6 1	cab	$$class\left\{x|\wr x^{-1}\in \mathrm{CnvRefRels}\right\}$$
8	0 7	wceq	$$wff\mathrm{Disjss}=\left\{x|\wr x^{-1}\in \mathrm{CnvRefRels}\right\}$$