Metamath Proof Explorer

Theorem elrels6

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

Ref Expression
Assertion elrels6 
|- ( R e. V -> ( R e. Rels <-> ( R i^i ( dom R X. ran R ) ) = R ) )

Proof

Step Hyp Ref Expression
1 elrelsrel 
 |-  ( R e. V -> ( R e. Rels <-> Rel R ) )
2 dfrel6 
 |-  ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R )
3 1 2 bitrdi 
 |-  ( R e. V -> ( R e. Rels <-> ( R i^i ( dom R X. ran R ) ) = R ) )