Theorem fvmpt4d

Description: Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 15-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fvmpt4d.1	|- F/_ x A
2		fvmpt4d.2	|- ( ph -> B e. C )
3		fvmpt4d.3	|- ( ph -> x e. A )
4	1	fvmpt2f	|- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )
5	3 2 4	syl2anc	|- ( ph -> ( ( x e. A |-> B ) ` x ) = B )