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	$$⊢\mathrm{Refs}=\left\{x|\left(\mathrm{I}\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefs	$$class\mathrm{Refs}$$
1		vx	$$setvarx$$
2		cid	$$class\mathrm{I}$$
3	1	cv	$$setvarx$$
4	3	cdm	$$class\mathrm{dom}x$$
5	3	crn	$$class\mathrm{ran}x$$
6	4 5	cxp	$$class\left(\mathrm{dom}x\times \mathrm{ran}x\right)$$
7	2 6	cin	$$class\left(\mathrm{I}\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)$$
8		cssr	$$class\mathrm{S}$$
9	3 6	cin	$$class\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)$$
10	7 9 8	wbr	$$wff\left(\mathrm{I}\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)$$
11	10 1	cab	$$class\left\{x|\left(\mathrm{I}\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\right\}$$
12	0 11	wceq	$$wff\mathrm{Refs}=\left\{x|\left(\mathrm{I}\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\right\}$$