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 ) )