Theorem dfrefrel5

Description: Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023)

	Ref	Expression
Assertion	dfrefrel5	⊢ ( RefRel 𝑅 ↔ ( ∀ 𝑥 ∈ ( dom 𝑅 ∩ ran 𝑅 ) 𝑥 𝑅 𝑥 ∧ Rel 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		dfrefrel2	⊢ ( RefRel 𝑅 ↔ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
2		ref5	⊢ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ ( dom 𝑅 ∩ ran 𝑅 ) 𝑥 𝑅 𝑥 )
3	1 2	bianbi	⊢ ( RefRel 𝑅 ↔ ( ∀ 𝑥 ∈ ( dom 𝑅 ∩ ran 𝑅 ) 𝑥 𝑅 𝑥 ∧ Rel 𝑅 ) )