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 𝐹 = ( 𝑥𝐸 , 𝑦𝐺𝐻 )
brovmptimex.br ( 𝜑𝐴 𝑅 𝐵 )
brovmptimex.ov ( 𝜑𝑅 = ( 𝐶 𝐹 𝐷 ) )
Assertion brovmptimex2 ( 𝜑𝐷 ∈ V )

Proof

Step Hyp Ref Expression
1 brovmptimex.mpt 𝐹 = ( 𝑥𝐸 , 𝑦𝐺𝐻 )
2 brovmptimex.br ( 𝜑𝐴 𝑅 𝐵 )
3 brovmptimex.ov ( 𝜑𝑅 = ( 𝐶 𝐹 𝐷 ) )
4 1 2 3 brovmptimex ( 𝜑 → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
5 4 simprd ( 𝜑𝐷 ∈ V )