df-trs

Description: Define the class of all transitive sets (versus the transitive class defined in df-tr ). It is used only by df-trrels .

		Ref	Expression
	Assertion	df-trs	$⊢ Trs = \{x \| ((x \cap (dom x \times ran x)) \circ (x \cap (dom x \times ran x))) S (x \cap (dom x \times ran x))\}$

Step	Hyp	Ref	Expression
0		ctrs	$class Trs$
1		vx	$setvar x$
2	1	cv	$setvar x$
3	2	cdm	$class dom x$
4	2	crn	$class ran x$
5	3 4	cxp	$class (dom x \times ran x)$
6	2 5	cin	$class (x \cap (dom x \times ran x))$
7	6 6	ccom	$class ((x \cap (dom x \times ran x)) \circ (x \cap (dom x \times ran x)))$
8		cssr	$class S$
9	7 6 8	wbr	$wff ((x \cap (dom x \times ran x)) \circ (x \cap (dom x \times ran x))) S (x \cap (dom x \times ran x))$
10	9 1	cab	$class \{x \| ((x \cap (dom x \times ran x)) \circ (x \cap (dom x \times ran x))) S (x \cap (dom x \times ran x))\}$
11	0 10	wceq	$wff Trs = \{x \| ((x \cap (dom x \times ran x)) \circ (x \cap (dom x \times ran x))) S (x \cap (dom x \times ran x))\}$

Metamath Proof Explorer