Metamath Proof Explorer


Theorem brovmptimex2

Description: If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021)

Ref Expression
Hypotheses brovmptimex.mpt F = x E , y G H
brovmptimex.br φ A R B
brovmptimex.ov φ R = C F D
Assertion brovmptimex2 φ D V

Proof

Step Hyp Ref Expression
1 brovmptimex.mpt F = x E , y G H
2 brovmptimex.br φ A R B
3 brovmptimex.ov φ R = C F D
4 1 2 3 brovmptimex φ C V D V
5 4 simprd φ D V