# Metamath Proof Explorer

## Theorem elrefrelsrel

Description: For sets, being an element of the class of reflexive relations ( df-refrels ) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021)

Ref Expression
Assertion elrefrelsrel ${⊢}{R}\in {V}\to \left({R}\in \mathrm{RefRels}↔RefRel{R}\right)$

### Proof

Step Hyp Ref Expression
1 elrelsrel ${⊢}{R}\in {V}\to \left({R}\in \mathrm{Rels}↔\mathrm{Rel}{R}\right)$
2 1 anbi2d ${⊢}{R}\in {V}\to \left(\left(\mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\wedge {R}\in \mathrm{Rels}\right)↔\left(\mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\wedge \mathrm{Rel}{R}\right)\right)$
3 elrefrels2 ${⊢}{R}\in \mathrm{RefRels}↔\left(\mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\wedge {R}\in \mathrm{Rels}\right)$
4 dfrefrel2 ${⊢}RefRel{R}↔\left(\mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\wedge \mathrm{Rel}{R}\right)$
5 2 3 4 3bitr4g ${⊢}{R}\in {V}\to \left({R}\in \mathrm{RefRels}↔RefRel{R}\right)$