Theorem fvmpt3i

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	|- ( x = A -> B = C )
	fvmpt3.b	|- F = ( x e. D |-> B )
	fvmpt3i.c	|- B e. _V
Assertion	fvmpt3i	|- ( A e. D -> ( F ` A ) = C )

Proof

Step	Hyp	Ref	Expression
1		fvmpt3.a	|- ( x = A -> B = C )
2		fvmpt3.b	|- F = ( x e. D |-> B )
3		fvmpt3i.c	|- B e. _V
4	3	a1i	|- ( x e. D -> B e. _V )
5	1 2 4	fvmpt3	|- ( A e. D -> ( F ` A ) = C )