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}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
Assertion ovmpt4g ${⊢}\left({x}\in {A}\wedge {y}\in {B}\wedge {C}\in {V}\right)\to {x}{F}{y}={C}$

Proof

Step Hyp Ref Expression
1 ovmpt4g.3 ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
2 elisset ${⊢}{C}\in {V}\to \exists {z}\phantom{\rule{.4em}{0ex}}{z}={C}$
3 moeq ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{z}={C}$
4 3 a1i ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to {\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{z}={C}$
5 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
6 1 5 eqtri ${⊢}{F}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
7 4 6 ovidi ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({z}={C}\to {x}{F}{y}={z}\right)$
8 eqeq2 ${⊢}{z}={C}\to \left({x}{F}{y}={z}↔{x}{F}{y}={C}\right)$
9 7 8 mpbidi ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({z}={C}\to {x}{F}{y}={C}\right)$
10 9 exlimdv ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}{z}={C}\to {x}{F}{y}={C}\right)$
11 2 10 syl5 ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({C}\in {V}\to {x}{F}{y}={C}\right)$
12 11 3impia ${⊢}\left({x}\in {A}\wedge {y}\in {B}\wedge {C}\in {V}\right)\to {x}{F}{y}={C}$