Theorem ovres

Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006)

	Ref	Expression
Assertion	ovres	$$⊢\left(A\in C\wedge B\in D\right)\to A\left({F\upharpoonright }_{\left(C\times D\right)}\right)B=AFB$$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$$⊢\left(A\in C\wedge B\in D\right)\to ⟨A,B⟩\in \left(C\times D\right)$$
2	1	fvresd	$$⊢\left(A\in C\wedge B\in D\right)\to \left({F\upharpoonright }_{\left(C\times D\right)}\right)\left(⟨A,B⟩\right)=F\left(⟨A,B⟩\right)$$
3		df-ov	$$⊢A\left({F\upharpoonright }_{\left(C\times D\right)}\right)B=\left({F\upharpoonright }_{\left(C\times D\right)}\right)\left(⟨A,B⟩\right)$$
4		df-ov	$$⊢AFB=F\left(⟨A,B⟩\right)$$
5	2 3 4	3eqtr4g	$$⊢\left(A\in C\wedge B\in D\right)\to A\left({F\upharpoonright }_{\left(C\times D\right)}\right)B=AFB$$