This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )