Metamath Proof Explorer


Theorem fvmpt2f

Description: Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017)

Ref Expression
Hypothesis fvmpt2f.0 _ x A
Assertion fvmpt2f x A B C x A B x = B

Proof

Step Hyp Ref Expression
1 fvmpt2f.0 _ x A
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 A
6 nfcv _ y B
7 nfcsb1v _ x y / x B
8 csbeq1a x = y B = y / x B
9 1 5 6 7 8 cbvmptf x A B = y A y / x B
10 4 9 fvmptg x A B C x A B x = B