Metamath Proof Explorer

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	$⊢ O = (x \in V, y \in V ⟼ \{⟨z, w⟩ \| φ\})$
	Assertion	brovmpoex	$⊢ F (V O E) P \to ((V \in V \land E \in V) \land (F \in V \land P \in V))$

Step	Hyp	Ref	Expression
1		brovmpoex.1	$⊢ O = (x \in V, y \in V ⟼ \{⟨z, w⟩ \| φ\})$
2	1	relmpoopab	$⊢ Rel (V O E)$
3	2	a1i	$⊢ (V \in V \land E \in V) \to Rel (V O E)$
4	1 3	brovex	$⊢ F (V O E) P \to ((V \in V \land E \in V) \land (F \in V \land P \in V))$