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 A B
Assertion fvmpt2i x A F x = I B

Proof

Step Hyp Ref Expression
1 mptrcl.1 F = x 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 _ y B
6 nfcsb1v _ x y / x B
7 csbeq1a x = y B = y / x B
8 5 6 7 cbvmpt x A B = y A y / x B
9 1 8 eqtri F = y A y / x B
10 4 9 fvmpti x A F x = I B