**Description:** Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013)

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

Hypothesis | seqeqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |

Assertion | seqeq1d | ⊢ ( 𝜑 → seq 𝐴 ( + , 𝐹 ) = seq 𝐵 ( + , 𝐹 ) ) |

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

1 | seqeqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |

2 | seqeq1 | ⊢ ( 𝐴 = 𝐵 → seq 𝐴 ( + , 𝐹 ) = seq 𝐵 ( + , 𝐹 ) ) | |

3 | 1 2 | syl | ⊢ ( 𝜑 → seq 𝐴 ( + , 𝐹 ) = seq 𝐵 ( + , 𝐹 ) ) |