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 e. V -> ( R e. RefRels <-> RefRel R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elrelsrel | |- ( R e. V -> ( R e. Rels <-> Rel R ) ) |
|
| 2 | 1 | anbi2d | |- ( R e. V -> ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ R e. Rels ) <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) ) ) |
| 3 | elrefrels2 | |- ( R e. RefRels <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ R e. Rels ) ) |
|
| 4 | dfrefrel2 | |- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) ) |
|
| 5 | 2 3 4 | 3bitr4g | |- ( R e. V -> ( R e. RefRels <-> RefRel R ) ) |