Description: The element of the relations class ( df-rels ) and the relation predicate are the same when R is a set. (Contributed by Peter Mazsa, 24-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | elrelsrel | |- ( R e. V -> ( R e. Rels <-> Rel R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrels2 | |- ( R e. V -> ( R e. Rels <-> R C_ ( _V X. _V ) ) ) |
|
2 | df-rel | |- ( Rel R <-> R C_ ( _V X. _V ) ) |
|
3 | 1 2 | bitr4di | |- ( R e. V -> ( R e. Rels <-> Rel R ) ) |