Theorem ovmpo

Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

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

Proof

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