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 ) )