Description: For sets, being an element of the class of converse reflexive relations ( df-cnvrefrels ) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | elcnvrefrelsrel | |- ( R e. V -> ( R e. CnvRefRels <-> CnvRefRel R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrelsrel | |- ( R e. V -> ( R e. Rels <-> Rel R ) ) |
|
2 | 1 | anbi2d | |- ( R e. V -> ( ( R C_ ( _I i^i ( dom R X. ran R ) ) /\ R e. Rels ) <-> ( R C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) ) ) |
3 | elcnvrefrels2 | |- ( R e. CnvRefRels <-> ( R C_ ( _I i^i ( dom R X. ran R ) ) /\ R e. Rels ) ) |
|
4 | dfcnvrefrel2 | |- ( CnvRefRel R <-> ( R C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) ) |
|
5 | 2 3 4 | 3bitr4g | |- ( R e. V -> ( R e. CnvRefRels <-> CnvRefRel R ) ) |