**Description:** Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 7-Dec-2014)

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

Hypotheses | ovmpod.1 | $${\u22a2}{\phi}\to {F}=\left({x}\in {C},{y}\in {D}\u27fc{R}\right)$$ | |

ovmpod.2 | $${\u22a2}\left({\phi}\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}={S}$$ | ||

ovmpod.3 | $${\u22a2}{\phi}\to {A}\in {C}$$ | ||

ovmpod.4 | $${\u22a2}{\phi}\to {B}\in {D}$$ | ||

ovmpod.5 | $${\u22a2}{\phi}\to {S}\in {X}$$ | ||

Assertion | ovmpod | $${\u22a2}{\phi}\to {A}{F}{B}={S}$$ |

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

1 | ovmpod.1 | $${\u22a2}{\phi}\to {F}=\left({x}\in {C},{y}\in {D}\u27fc{R}\right)$$ | |

2 | ovmpod.2 | $${\u22a2}\left({\phi}\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}={S}$$ | |

3 | ovmpod.3 | $${\u22a2}{\phi}\to {A}\in {C}$$ | |

4 | ovmpod.4 | $${\u22a2}{\phi}\to {B}\in {D}$$ | |

5 | ovmpod.5 | $${\u22a2}{\phi}\to {S}\in {X}$$ | |

6 | eqidd | $${\u22a2}\left({\phi}\wedge {x}={A}\right)\to {D}={D}$$ | |

7 | 1 2 6 3 4 5 | ovmpodx | $${\u22a2}{\phi}\to {A}{F}{B}={S}$$ |