Theorem dfcnvrefrel5

Description: Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024)

	Ref	Expression
Assertion	dfcnvrefrel5	⊢ ( CnvRefRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ Rel 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		dfcnvrefrel4	⊢ ( CnvRefRel 𝑅 ↔ ( 𝑅 ⊆ I ∧ Rel 𝑅 ) )
2		cnvref5	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) )
3	1 2	bianim	⊢ ( CnvRefRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ∧ Rel 𝑅 ) )