Metamath Proof Explorer


Theorem brovmptimex1

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. E , y e. G |-> H )
brovmptimex.br
|- ( ph -> A R B )
brovmptimex.ov
|- ( ph -> R = ( C F D ) )
Assertion brovmptimex1
|- ( ph -> C e. _V )

Proof

Step Hyp Ref Expression
1 brovmptimex.mpt
 |-  F = ( x e. E , y e. G |-> H )
2 brovmptimex.br
 |-  ( ph -> A R B )
3 brovmptimex.ov
 |-  ( ph -> R = ( C F D ) )
4 1 2 3 brovmptimex
 |-  ( ph -> ( C e. _V /\ D e. _V ) )
5 4 simpld
 |-  ( ph -> C e. _V )