Metamath Proof Explorer

Theorem elrels5

Description: Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021)

Ref Expression
Assertion elrels5 
|- ( R e. V -> ( R e. Rels <-> ( R |` dom R ) = R ) )

Proof

Step Hyp Ref Expression
1 elrelsrel 
 |-  ( R e. V -> ( R e. Rels <-> Rel R ) )
2 dfrel5 
 |-  ( Rel R <-> ( R |` dom R ) = R )
3 1 2 bitrdi 
 |-  ( R e. V -> ( R e. Rels <-> ( R |` dom R ) = R ) )