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

Metamath Proof Explorer

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^{-1} \in CnvRefRels\}$

Detailed syntax breakdown

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