Description: The element of the relations class ( df-rels ) and the relation predicate ( df-rel ) are the same when R is a set. (Contributed by Peter Mazsa, 14-Jun-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | elrels2 | |- ( R e. V -> ( R e. Rels <-> R C_ ( _V X. _V ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rels | |- Rels = ~P ( _V X. _V ) |
|
2 | 1 | eleq2i | |- ( R e. Rels <-> R e. ~P ( _V X. _V ) ) |
3 | elpwg | |- ( R e. V -> ( R e. ~P ( _V X. _V ) <-> R C_ ( _V X. _V ) ) ) |
|
4 | 2 3 | syl5bb | |- ( R e. V -> ( R e. Rels <-> R C_ ( _V X. _V ) ) ) |