Theorem ovmpoa

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

	Ref	Expression
Hypotheses	ovmpoga.1	$$⊢\left(x=A\wedge y=B\right)\to R=S$$
	ovmpoga.2	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
	ovmpoa.4	$$⊢S\in \mathrm{V}$$
Assertion	ovmpoa	$$⊢\left(A\in C\wedge B\in D\right)\to AFB=S$$

Proof

Step	Hyp	Ref	Expression
1		ovmpoga.1	$$⊢\left(x=A\wedge y=B\right)\to R=S$$
2		ovmpoga.2	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
3		ovmpoa.4	$$⊢S\in \mathrm{V}$$
4	1 2	ovmpoga	$$⊢\left(A\in C\wedge B\in D\wedge S\in \mathrm{V}\right)\to AFB=S$$
5	3 4	mp3an3	$$⊢\left(A\in C\wedge B\in D\right)\to AFB=S$$