Theorem elrefrels2

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

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

Proof

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