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 e. _V , y e. _V |-> { <. z , w >. | ph } )
Assertion	brovmpoex	|- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )

Proof

Step	Hyp	Ref	Expression
1		brovmpoex.1	|- O = ( x e. _V , y e. _V |-> { <. z , w >. | ph } )
2	1	relmpoopab	|- Rel ( V O E )
3	2	a1i	|- ( ( V e. _V /\ E e. _V ) -> Rel ( V O E ) )
4	1 3	brovex	|- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )