Definition df-refs

Description: Define the class of all reflexive sets. It is used only by df-refrels . We use subset relation _S ( df-ssr ) here to be able to define converse reflexivity ( df-cnvrefs ), see also the comment of df-ssr . The elements of this class are not necessarily relations (versus df-refrels ).

Note the similarity of Definitions df-refs , df-syms and df-trs , cf. comments of dfrefrels2 . (Contributed by Peter Mazsa, 19-Jul-2019)

	Ref	Expression
Assertion	df-refs	|- Refs = { 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		crefs	|- Refs
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	3 6	cin	|- ( x i^i ( dom x X. ran x ) )
10	7 9 8	wbr	|- ( _I i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) )
11	10 1	cab	|- { x | ( _I i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) ) }
12	0 11	wceq	|- Refs = { x | ( _I i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) ) }