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=xA,yBC
Assertion ovmpt4g xAyBCVxFy=C

Proof

Step Hyp Ref Expression
1 ovmpt4g.3 F=xA,yBC
2 elisset CVzz=C
3 moeq *zz=C
4 3 a1i xAyB*zz=C
5 df-mpo xA,yBC=xyz|xAyBz=C
6 1 5 eqtri F=xyz|xAyBz=C
7 4 6 ovidi xAyBz=CxFy=z
8 eqeq2 z=CxFy=zxFy=C
9 7 8 mpbidi xAyBz=CxFy=C
10 9 exlimdv xAyBzz=CxFy=C
11 2 10 syl5 xAyBCVxFy=C
12 11 3impia xAyBCVxFy=C