Metamath Proof Explorer

Theorem fvmpti

Description: Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 fvmptg.1 
 |-  ( x = A -> B = C )
2 fvmptg.2 
 |-  F = ( x e. D |-> B )
3 1 2 fvmptg 
 |-  ( ( A e. D /\ C e. _V ) -> ( F ` A ) = C )
4 fvi 
 |-  ( C e. _V -> ( _I ` C ) = C )
5 4 adantl 
 |-  ( ( A e. D /\ C e. _V ) -> ( _I ` C ) = C )
6 3 5 eqtr4d 
 |-  ( ( A e. D /\ C e. _V ) -> ( F ` A ) = ( _I ` C ) )
7 1 eleq1d 
 |-  ( x = A -> ( B e. _V <-> C e. _V ) )
8 2 dmmpt 
 |-  dom F = { x e. D | B e. _V }
9 7 8 elrab2 
 |-  ( A e. dom F <-> ( A e. D /\ C e. _V ) )
10 9 baib 
 |-  ( A e. D -> ( A e. dom F <-> C e. _V ) )
11 10 notbid 
 |-  ( A e. D -> ( -. A e. dom F <-> -. C e. _V ) )
12 ndmfv 
 |-  ( -. A e. dom F -> ( F ` A ) = (/) )
13 11 12 syl6bir 
 |-  ( A e. D -> ( -. C e. _V -> ( F ` A ) = (/) ) )
14 13 imp 
 |-  ( ( A e. D /\ -. C e. _V ) -> ( F ` A ) = (/) )
15 fvprc 
 |-  ( -. C e. _V -> ( _I ` C ) = (/) )
16 15 adantl 
 |-  ( ( A e. D /\ -. C e. _V ) -> ( _I ` C ) = (/) )
17 14 16 eqtr4d 
 |-  ( ( A e. D /\ -. C e. _V ) -> ( F ` A ) = ( _I ` C ) )
18 6 17 pm2.61dan 
 |-  ( A e. D -> ( F ` A ) = ( _I ` C ) )