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 defAt <. A , B >. -> (( A F B )) = ( A F B ) )

Proof

Step	Hyp	Ref	Expression
1		afvfundmfveq	|- ( F defAt <. A , B >. -> ( F ''' <. A , B >. ) = ( F ` <. A , B >. ) )
2		df-aov	|- (( A F B )) = ( F ''' <. A , B >. )
3		df-ov	|- ( A F B ) = ( F ` <. A , B >. )
4	1 2 3	3eqtr4g	|- ( F defAt <. A , B >. -> (( A F B )) = ( A F B ) )