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	⊢ ( 𝜑 → 𝐹 = 𝐺 )
	afveq12d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	afveq12d	⊢ ( 𝜑 → ( 𝐹 ''' 𝐴 ) = ( 𝐺 ''' 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		afveq12d.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
2		afveq12d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	1 2	dfateq12d	⊢ ( 𝜑 → ( 𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵 ) )
4	1 2	fveq12d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐵 ) )
5	3 4	ifbieq1d	⊢ ( 𝜑 → if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = if ( 𝐺 defAt 𝐵 , ( 𝐺 ‘ 𝐵 ) , V ) )
6		dfafv2	⊢ ( 𝐹 ''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V )
7		dfafv2	⊢ ( 𝐺 ''' 𝐵 ) = if ( 𝐺 defAt 𝐵 , ( 𝐺 ‘ 𝐵 ) , V )
8	5 6 7	3eqtr4g	⊢ ( 𝜑 → ( 𝐹 ''' 𝐴 ) = ( 𝐺 ''' 𝐵 ) )