Theorem ovmpoa

Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013)

	Ref	Expression
Hypotheses	ovmpoga.1	|- ( ( x = A /\ y = B ) -> R = S )
	ovmpoga.2	|- F = ( x e. C , y e. D |-> R )
	ovmpoa.4	|- S e. _V
Assertion	ovmpoa	|- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )

Proof

Step	Hyp	Ref	Expression
1		ovmpoga.1	|- ( ( x = A /\ y = B ) -> R = S )
2		ovmpoga.2	|- F = ( x e. C , y e. D |-> R )
3		ovmpoa.4	|- S e. _V
4	1 2	ovmpoga	|- ( ( A e. C /\ B e. D /\ S e. _V ) -> ( A F B ) = S )
5	3 4	mp3an3	|- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )