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