Theorem fvmpt2df

Description: Deduction version of fvmpt2 . (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	fvmpt2df.1	|- F/_ x A
	fvmpt2df.2	|- F = ( x e. A |-> B )
	fvmpt2df.3	|- ( ( ph /\ x e. A ) -> B e. V )
Assertion	fvmpt2df	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2df.1	|- F/_ x A
2		fvmpt2df.2	|- F = ( x e. A |-> B )
3		fvmpt2df.3	|- ( ( ph /\ x e. A ) -> B e. V )
4	2	fveq1i	|- ( F ` x ) = ( ( x e. A |-> B ) ` x )
5		id	|- ( x e. A -> x e. A )
6	1	fvmpt2f	|- ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
7	5 3 6	syl2an2	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
8	4 7	eqtrid	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )