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 = { 𝑥 ∣ ≀ ◡ 𝑥 ∈ CnvRefRels }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdisjss	⊢ Disjss
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	ccnv	⊢ ◡ 𝑥
4	3	ccoss	⊢ ≀ ◡ 𝑥
5		ccnvrefrels	⊢ CnvRefRels
6	4 5	wcel	⊢ ≀ ◡ 𝑥 ∈ CnvRefRels
7	6 1	cab	⊢ { 𝑥 ∣ ≀ ◡ 𝑥 ∈ CnvRefRels }
8	0 7	wceq	⊢ Disjss = { 𝑥 ∣ ≀ ◡ 𝑥 ∈ CnvRefRels }