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 𝐹 = ( 𝑥𝐴𝐵 )
Assertion fvmpt2i ( 𝑥𝐴 → ( 𝐹𝑥 ) = ( I ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mptrcl.1 𝐹 = ( 𝑥𝐴𝐵 )
2 csbeq1 ( 𝑦 = 𝑥 𝑦 / 𝑥 𝐵 = 𝑥 / 𝑥 𝐵 )
3 csbid 𝑥 / 𝑥 𝐵 = 𝐵
4 2 3 eqtrdi ( 𝑦 = 𝑥 𝑦 / 𝑥 𝐵 = 𝐵 )
5 nfcv 𝑦 𝐵
6 nfcsb1v 𝑥 𝑦 / 𝑥 𝐵
7 csbeq1a ( 𝑥 = 𝑦𝐵 = 𝑦 / 𝑥 𝐵 )
8 5 6 7 cbvmpt ( 𝑥𝐴𝐵 ) = ( 𝑦𝐴 𝑦 / 𝑥 𝐵 )
9 1 8 eqtri 𝐹 = ( 𝑦𝐴 𝑦 / 𝑥 𝐵 )
10 4 9 fvmpti ( 𝑥𝐴 → ( 𝐹𝑥 ) = ( I ‘ 𝐵 ) )