# Metamath Proof Explorer

## Theorem ovmpoga

Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses ovmpoga.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to {R}={S}$
ovmpoga.2 ${⊢}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
Assertion ovmpoga ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in {H}\right)\to {A}{F}{B}={S}$

### Proof

Step Hyp Ref Expression
1 ovmpoga.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to {R}={S}$
2 ovmpoga.2 ${⊢}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
3 elex ${⊢}{S}\in {H}\to {S}\in \mathrm{V}$
4 2 a1i ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in \mathrm{V}\right)\to {F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
5 1 adantl ${⊢}\left(\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in \mathrm{V}\right)\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}={S}$
6 simp1 ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in \mathrm{V}\right)\to {A}\in {C}$
7 simp2 ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in \mathrm{V}\right)\to {B}\in {D}$
8 simp3 ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in \mathrm{V}\right)\to {S}\in \mathrm{V}$
9 4 5 6 7 8 ovmpod ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in \mathrm{V}\right)\to {A}{F}{B}={S}$
10 3 9 syl3an3 ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {S}\in {H}\right)\to {A}{F}{B}={S}$