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=\left(x\in E,y\in G⟼H\right)$$
	brovmptimex.br	$$⊢\phi \to ARB$$
	brovmptimex.ov	$$⊢\phi \to R=CFD$$
Assertion	brovmptimex2	$$⊢\phi \to D\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		brovmptimex.mpt	$$⊢F=\left(x\in E,y\in G⟼H\right)$$
2		brovmptimex.br	$$⊢\phi \to ARB$$
3		brovmptimex.ov	$$⊢\phi \to R=CFD$$
4	1 2 3	brovmptimex	$$⊢\phi \to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
5	4	simprd	$$⊢\phi \to D\in \mathrm{V}$$