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 ) |
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 ) |