Metamath Proof Explorer


Theorem ovmpt4g

Description: Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 .) (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypothesis ovmpt4g.3 F = x A , y B C
Assertion ovmpt4g x A y B C V x F y = C

Proof

Step Hyp Ref Expression
1 ovmpt4g.3 F = x A , y B C
2 elisset C V z z = C
3 moeq * z z = C
4 3 a1i x A y B * z z = C
5 df-mpo x A , y B C = x y z | x A y B z = C
6 1 5 eqtri F = x y z | x A y B z = C
7 4 6 ovidi x A y B z = C x F y = z
8 eqeq2 z = C x F y = z x F y = C
9 7 8 mpbidi x A y B z = C x F y = C
10 9 exlimdv x A y B z z = C x F y = C
11 2 10 syl5 x A y B C V x F y = C
12 11 3impia x A y B C V x F y = C