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 >. e. ( R |` X ) -> A e. X )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( <. A , B >. e. ( R i^i ( X X. _V ) ) <-> ( <. A , B >. e. R /\ <. A , B >. e. ( X X. _V ) ) )
2		opelxp1	|- ( <. A , B >. e. ( X X. _V ) -> A e. X )
3	1 2	simplbiim	|- ( <. A , B >. e. ( R i^i ( X X. _V ) ) -> A e. X )
4		df-res	|- ( R |` X ) = ( R i^i ( X X. _V ) )
5	3 4	eleq2s	|- ( <. A , B >. e. ( R |` X ) -> A e. X )