Theorem fvmpt2i

Description: Value of a function given by the maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypothesis	mptrcl.1	|- F = ( x e. A |-> B )
Assertion	fvmpt2i	|- ( x e. A -> ( F ` x ) = ( _I ` B ) )

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	|- F = ( x e. A |-> B )
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 B
6		nfcsb1v	|- F/_ x [_ y / x ]_ B
7		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
8	5 6 7	cbvmpt	|- ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
9	1 8	eqtri	|- F = ( y e. A |-> [_ y / x ]_ B )
10	4 9	fvmpti	|- ( x e. A -> ( F ` x ) = ( _I ` B ) )