Metamath Proof Explorer

Theorem dfrefrels3

Description: Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019)

Ref Expression
Assertion dfrefrels3 ⊢ RefRels = r ∈ Rels | ∀ x ∈ dom ⁡ r ∀ y ∈ ran ⁡ r x = y → x r y

Proof

Step Hyp Ref Expression
1 dfrefrels2 ⊢ RefRels = r ∈ Rels | I ∩ dom ⁡ r × ran ⁡ r ⊆ r
2 idinxpss ⊢ I ∩ dom ⁡ r × ran ⁡ r ⊆ r ↔ ∀ x ∈ dom ⁡ r ∀ y ∈ ran ⁡ r x = y → x r y
3 1 2 rabbieq ⊢ RefRels = r ∈ Rels | ∀ x ∈ dom ⁡ r ∀ y ∈ ran ⁡ r x = y → x r y