Theorem fvmpt2f

Description: Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017)

	Ref	Expression
Hypothesis	fvmpt2f.0	|- F/_ x A
Assertion	fvmpt2f	|- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2f.0	|- F/_ x A
2		csbeq1	|- ( y = x -> [_ y / x ]_ B = [_ x / x ]_ B )
3		csbid	|- [_ x / x ]_ B = B
4	2 3	eqtrdi	|- ( y = x -> [_ y / x ]_ B = B )
5		nfcv	|- F/_ y A
6		nfcv	|- F/_ y B
7		nfcsb1v	|- F/_ x [_ y / x ]_ B
8		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
9	1 5 6 7 8	cbvmptf	|- ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
10	4 9	fvmptg	|- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )