Metamath Proof Explorer

Definition df-cnvrefs

Description: Define the class of all converse reflexive sets, see the comment of df-ssr . It is used only by df-cnvrefrels . (Contributed by Peter Mazsa, 22-Jul-2019)

		Ref	Expression
	Assertion	df-cnvrefs	$⊢ CnvRefs = \{x \| (I \cap (dom x \times ran x)) S^{-1} (x \cap (dom x \times ran x))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnvrefs	$class CnvRefs$
1		vx	$setvar x$
2		cid	$class I$
3	1	cv	$setvar x$
4	3	cdm	$class dom x$
5	3	crn	$class ran x$
6	4 5	cxp	$class (dom x \times ran x)$
7	2 6	cin	$class (I \cap (dom x \times ran x))$
8		cssr	$class S$
9	8	ccnv	$class S^{-1}$
10	3 6	cin	$class (x \cap (dom x \times ran x))$
11	7 10 9	wbr	$wff (I \cap (dom x \times ran x)) S^{-1} (x \cap (dom x \times ran x))$
12	11 1	cab	$class \{x \| (I \cap (dom x \times ran x)) S^{-1} (x \cap (dom x \times ran x))\}$
13	0 12	wceq	$wff CnvRefs = \{x \| (I \cap (dom x \times ran x)) S^{-1} (x \cap (dom x \times ran x))\}$