Theorem elcnvrefrels2

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019)

	Ref	Expression
Assertion	elcnvrefrels2	⊢ ( 𝑅 ∈ CnvRefRels ↔ ( 𝑅 ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dfcnvrefrels2	⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) }
2		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
3		dmeq	⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
4		rneq	⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 )
5	3 4	xpeq12d	⊢ ( 𝑟 = 𝑅 → ( dom 𝑟 × ran 𝑟 ) = ( dom 𝑅 × ran 𝑅 ) )
6	5	ineq2d	⊢ ( 𝑟 = 𝑅 → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) = ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) )
7	2 6	sseq12d	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ 𝑅 ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ) )
8	1 7	rabeqel	⊢ ( 𝑅 ∈ CnvRefRels ↔ ( 𝑅 ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ 𝑅 ∈ Rels ) )