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

Proof

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