Theorem brovmpoex

Description: A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017)

	Ref	Expression
Hypothesis	brovmpoex.1	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜑 } )
Assertion	brovmpoex	⊢ ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )

Proof

Step	Hyp	Ref	Expression
1		brovmpoex.1	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜑 } )
2	1	relmpoopab	⊢ Rel ( 𝑉 𝑂 𝐸 )
3	2	a1i	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → Rel ( 𝑉 𝑂 𝐸 ) )
4	1 3	brovex	⊢ ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )