**Description:** Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017)

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

Hypothesis | prodeq2dv.1 | $${\u22a2}\left({\phi}\wedge {k}\in {A}\right)\to {B}={C}$$ | |

Assertion | prodeq2dv | $${\u22a2}{\phi}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ |

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

1 | prodeq2dv.1 | $${\u22a2}\left({\phi}\wedge {k}\in {A}\right)\to {B}={C}$$ | |

2 | 1 | ralrimiva | $${\u22a2}{\phi}\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}$$ |

3 | 2 | prodeq2d | $${\u22a2}{\phi}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ |