Theorem fvmpts

Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	fvmpts.1	|- F = ( x e. C |-> B )
Assertion	fvmpts	|- ( ( A e. C /\ [_ A / x ]_ B e. V ) -> ( F ` A ) = [_ A / x ]_ B )

Proof

Step	Hyp	Ref	Expression
1		fvmpts.1	|- F = ( x e. C |-> B )
2		csbeq1	|- ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
3		nfcv	|- F/_ y B
4		nfcsb1v	|- F/_ x [_ y / x ]_ B
5		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
6	3 4 5	cbvmpt	|- ( x e. C |-> B ) = ( y e. C |-> [_ y / x ]_ B )
7	1 6	eqtri	|- F = ( y e. C |-> [_ y / x ]_ B )
8	2 7	fvmptg	|- ( ( A e. C /\ [_ A / x ]_ B e. V ) -> ( F ` A ) = [_ A / x ]_ B )