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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnvrefs	⊢ CnvRefs
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	8	ccnv	⊢ ◡ S
10	3 6	cin	⊢ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
11	7 10 9	wbr	⊢ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) ◡ S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
12	11 1	cab	⊢ { 𝑥 ∣ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) ◡ S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }
13	0 12	wceq	⊢ CnvRefs = { 𝑥 ∣ ( I ∩ ( dom 𝑥 × ran 𝑥 ) ) ◡ S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }