Metamath Proof Explorer

Theorem dfrefrel5

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

Ref Expression
Assertion dfrefrel5 ⊢ RefRel R ↔ ∀ x ∈ dom ⁡ R ∩ ran ⁡ R x R x ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dfrefrel2 ⊢ RefRel R ↔ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∧ Rel ⁡ R
2 ref5 ⊢ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ↔ ∀ x ∈ dom ⁡ R ∩ ran ⁡ R x R x
3 1 2 bianbi ⊢ RefRel R ↔ ∀ x ∈ dom ⁡ R ∩ ran ⁡ R x R x ∧ Rel ⁡ R