Theorem fvmptd4

Description: Deduction version of fvmpt (where the substitution hypothesis does not have the antecedent ph ). (Contributed by SN, 26-Jul-2024)

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

Proof

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