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 V R Rels R dom R = R

Proof

Step Hyp Ref Expression
1 elrelsrel R V R Rels Rel R
2 dfrel5 Rel R R dom R = R
3 1 2 bitrdi R V R Rels R dom R = R