Theorem ovmpog

Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999) (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)$$
Assertion	ovmpog	$$⊢\left(A\in C\wedge B\in D\wedge S\in H\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	1 2	sylan9eq	$$⊢\left(x=A\wedge y=B\right)\to R=S$$
5	4 3	ovmpoga	$$⊢\left(A\in C\wedge B\in D\wedge S\in H\right)\to AFB=S$$