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	|- Disjss = { x | ,~ `' x e. CnvRefRels }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdisjss	|- Disjss
1		vx	|- x
2	1	cv	|- x
3	2	ccnv	|- `' x
4	3	ccoss	|- ,~ `' x
5		ccnvrefrels	|- CnvRefRels
6	4 5	wcel	|- ,~ `' x e. CnvRefRels
7	6 1	cab	|- { x | ,~ `' x e. CnvRefRels }
8	0 7	wceq	|- Disjss = { x | ,~ `' x e. CnvRefRels }