**Description:** Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014)

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

Hypotheses | reseqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |

reseqd.2 | ⊢ ( 𝜑 → 𝐶 = 𝐷 ) | ||

Assertion | reseq12d | ⊢ ( 𝜑 → ( 𝐴 ↾ 𝐶 ) = ( 𝐵 ↾ 𝐷 ) ) |

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

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

2 | reseqd.2 | ⊢ ( 𝜑 → 𝐶 = 𝐷 ) | |

3 | 1 | reseq1d | ⊢ ( 𝜑 → ( 𝐴 ↾ 𝐶 ) = ( 𝐵 ↾ 𝐶 ) ) |

4 | 2 | reseq2d | ⊢ ( 𝜑 → ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ↾ 𝐷 ) ) |

5 | 3 4 | eqtrd | ⊢ ( 𝜑 → ( 𝐴 ↾ 𝐶 ) = ( 𝐵 ↾ 𝐷 ) ) |