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 i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnvrefs	|- CnvRefs
1		vx	|- x
2		cid	|- _I
3	1	cv	|- x
4	3	cdm	|- dom x
5	3	crn	|- ran x
6	4 5	cxp	|- ( dom x X. ran x )
7	2 6	cin	|- ( _I i^i ( dom x X. ran x ) )
8		cssr	|- _S
9	8	ccnv	|- `' _S
10	3 6	cin	|- ( x i^i ( dom x X. ran x ) )
11	7 10 9	wbr	|- ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) )
12	11 1	cab	|- { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) }
13	0 12	wceq	|- CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) }