Metamath Proof Explorer


Theorem fvmpt2i

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

Ref Expression
Hypothesis mptrcl.1
|- F = ( x e. A |-> B )
Assertion fvmpt2i
|- ( x e. A -> ( F ` x ) = ( _I ` B ) )

Proof

Step Hyp Ref Expression
1 mptrcl.1
 |-  F = ( x e. A |-> B )
2 csbeq1
 |-  ( y = x -> [_ y / x ]_ B = [_ x / x ]_ B )
3 csbid
 |-  [_ x / x ]_ B = B
4 2 3 eqtrdi
 |-  ( y = x -> [_ y / x ]_ B = B )
5 nfcv
 |-  F/_ y B
6 nfcsb1v
 |-  F/_ x [_ y / x ]_ B
7 csbeq1a
 |-  ( x = y -> B = [_ y / x ]_ B )
8 5 6 7 cbvmpt
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
9 1 8 eqtri
 |-  F = ( y e. A |-> [_ y / x ]_ B )
10 4 9 fvmpti
 |-  ( x e. A -> ( F ` x ) = ( _I ` B ) )