Description: The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | elrelsrelim | |- ( R e. Rels -> Rel R ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrelsrel | |- ( R e. Rels -> ( R e. Rels <-> Rel R ) ) |
|
2 | 1 | ibi | |- ( R e. Rels -> Rel R ) |