Metamath Proof Explorer


Theorem brovpreldm

Description: If a binary relation holds for the result of an operation, the operands are in the domain of the operation. (Contributed by AV, 31-Dec-2020)

Ref Expression
Assertion brovpreldm
|- ( D ( B A C ) E -> <. B , C >. e. dom A )

Proof

Step Hyp Ref Expression
1 df-br
 |-  ( D ( B A C ) E <-> <. D , E >. e. ( B A C ) )
2 ne0i
 |-  ( <. D , E >. e. ( B A C ) -> ( B A C ) =/= (/) )
3 df-ov
 |-  ( B A C ) = ( A ` <. B , C >. )
4 ndmfv
 |-  ( -. <. B , C >. e. dom A -> ( A ` <. B , C >. ) = (/) )
5 3 4 eqtrid
 |-  ( -. <. B , C >. e. dom A -> ( B A C ) = (/) )
6 5 necon1ai
 |-  ( ( B A C ) =/= (/) -> <. B , C >. e. dom A )
7 2 6 syl
 |-  ( <. D , E >. e. ( B A C ) -> <. B , C >. e. dom A )
8 1 7 sylbi
 |-  ( D ( B A C ) E -> <. B , C >. e. dom A )