Theorem bj-brresdm

Description: If two classes are related by a restricted binary relation, then the first class is an element of the restricting class. See also brres and brrelex1 .

Remark: there are many pairs like bj-opelresdm / bj-brresdm , where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm / brrelex12 or the opelopabg / brabg family). They are straightforwardly equivalent by df-br . The latter is indeed a very direct definition, introducing a "shorthand", and barely necessary, were it not for the frequency of the expression A R B . Therefore, in the spirit of "definitions are here to be used", most theorems, apart from the most elementary ones, should only have the "br" version, not the "opel" one. (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Assertion	bj-brresdm	|- ( A ( R |` X ) B -> A e. X )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( A ( R |` X ) B <-> <. A , B >. e. ( R |` X ) )
2		bj-opelresdm	|- ( <. A , B >. e. ( R |` X ) -> A e. X )
3	1 2	sylbi	|- ( A ( R |` X ) B -> A e. X )