Theorem fvmptd3

Description: Deduction version of fvmpt . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fvmptd3.1	|- F = ( x e. D |-> B )
	fvmptd3.2	|- ( x = A -> B = C )
	fvmptd3.3	|- ( ph -> A e. D )
	fvmptd3.4	|- ( ph -> C e. V )
Assertion	fvmptd3	|- ( ph -> ( F ` A ) = C )

Proof

Step	Hyp	Ref	Expression
1		fvmptd3.1	|- F = ( x e. D |-> B )
2		fvmptd3.2	|- ( x = A -> B = C )
3		fvmptd3.3	|- ( ph -> A e. D )
4		fvmptd3.4	|- ( ph -> C e. V )
5	2 1	fvmptg	|- ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )
6	3 4 5	syl2anc	|- ( ph -> ( F ` A ) = C )