Theorem elcnvrefrels3

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021)

	Ref	Expression
Assertion	elcnvrefrels3	⊢ ( 𝑅 ∈ CnvRefRels ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dfcnvrefrels3	⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) }
2		dmeq	⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3		rneq	⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 )
4		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
5	4	imbi1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) )
6	3 5	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) )
7	2 6	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 𝑟 𝑦 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) )
8	1 7	rabeqel	⊢ ( 𝑅 ∈ CnvRefRels ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ 𝑅 ∈ Rels ) )