Theorem fvmpt3

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	|- ( x = A -> B = C )
	fvmpt3.b	|- F = ( x e. D |-> B )
	fvmpt3.c	|- ( x e. D -> B e. V )
Assertion	fvmpt3	|- ( 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		fvmpt3.c	|- ( x e. D -> B e. V )
4	1	eleq1d	|- ( x = A -> ( B e. V <-> C e. V ) )
5	4 3	vtoclga	|- ( A e. D -> C e. V )
6	1 2	fvmptg	|- ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )
7	5 6	mpdan	|- ( A e. D -> ( F ` A ) = C )