Metamath Proof Explorer

Theorem bj-opelresdm

Description: If an ordered pair is in a restricted binary relation, then its first component is an element of the restricting class. See also opelres . (Contributed by BJ, 25-Dec-2023)

Ref Expression
Assertion bj-opelresdm A B R X A X


Step Hyp Ref Expression
1 elin A B R X × V A B R A B X × V
2 opelxp1 A B X × V A X
3 1 2 simplbiim A B R X × V A X
4 df-res R X = R X × V
5 3 4 eleq2s A B R X A X