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

Ref | Expression | ||
---|---|---|---|

Hypotheses | ovmpoga.1 | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 ) | |

ovmpoga.2 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) | ||

ovmpoa.4 | ⊢ 𝑆 ∈ V | ||

Assertion | ovmpoa | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ovmpoga.1 | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑅 = 𝑆 ) | |

2 | ovmpoga.2 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) | |

3 | ovmpoa.4 | ⊢ 𝑆 ∈ V | |

4 | 1 2 | ovmpoga | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) |

5 | 3 4 | mp3an3 | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) |