Theorem fvmptg

Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	fvmptg.1	|- ( x = A -> B = C )
	fvmptg.2	|- F = ( x e. D |-> B )
Assertion	fvmptg	|- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

Proof

Step	Hyp	Ref	Expression
1		fvmptg.1	|- ( x = A -> B = C )
2		fvmptg.2	|- F = ( x e. D |-> B )
3		eqid	|- C = C
4	1	eqeq2d	|- ( x = A -> ( y = B <-> y = C ) )
5		eqeq1	|- ( y = C -> ( y = C <-> C = C ) )
6		moeq	|- E* y y = B
7	6	a1i	|- ( x e. D -> E* y y = B )
8		df-mpt	|- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	2 8	eqtri	|- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	4 5 7 9	fvopab3ig	|- ( ( A e. D /\ C e. R ) -> ( C = C -> ( F ` A ) = C ) )
11	3 10	mpi	|- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )