Theorem afveq12d

Description: Equality deduction for function value, analogous to fveq12d . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	afveq12d.1	|- ( ph -> F = G )
	afveq12d.2	|- ( ph -> A = B )
Assertion	afveq12d	|- ( ph -> ( F ''' A ) = ( G ''' B ) )

Proof

Step	Hyp	Ref	Expression
1		afveq12d.1	|- ( ph -> F = G )
2		afveq12d.2	|- ( ph -> A = B )
3	1 2	dfateq12d	|- ( ph -> ( F defAt A <-> G defAt B ) )
4	1 2	fveq12d	|- ( ph -> ( F ` A ) = ( G ` B ) )
5	3 4	ifbieq1d	|- ( ph -> if ( F defAt A , ( F ` A ) , _V ) = if ( G defAt B , ( G ` B ) , _V ) )
6		dfafv2	|- ( F ''' A ) = if ( F defAt A , ( F ` A ) , _V )
7		dfafv2	|- ( G ''' B ) = if ( G defAt B , ( G ` B ) , _V )
8	5 6 7	3eqtr4g	|- ( ph -> ( F ''' A ) = ( G ''' B ) )