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 = { 𝑥 ∣ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefs	⊢ Refs
1		vx	⊢ 𝑥
2		cid	⊢ I
3	1	cv	⊢ 𝑥
4	3	cdm	⊢ dom 𝑥
5	3	crn	⊢ ran 𝑥
6	4 5	cxp	⊢ ( dom 𝑥 × ran 𝑥 )
7	2 6	cin	⊢ ( I ∩ ( dom 𝑥 × ran 𝑥 ) )
8		cssr	⊢ S
9	3 6	cin	⊢ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
10	7 9 8	wbr	⊢ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
11	10 1	cab	⊢ { 𝑥 ∣ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }
12	0 11	wceq	⊢ Refs = { 𝑥 ∣ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }