Theorem aovfundmoveq

Description: If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	aovfundmoveq	$$⊢F\mathrm{defAt}⟨A,B⟩\to ((AFB))=AFB$$

Proof

Step	Hyp	Ref	Expression
1		afvfundmfveq	$$⊢F\mathrm{defAt}⟨A,B⟩\to \left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)=F\left(⟨A,B⟩\right)$$
2		df-aov	$$⊢((AFB))=\left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)$$
3		df-ov	$$⊢AFB=F\left(⟨A,B⟩\right)$$
4	1 2 3	3eqtr4g	$$⊢F\mathrm{defAt}⟨A,B⟩\to ((AFB))=AFB$$