**Description:** Equality deduction for a binary relation. (Contributed by Thierry
Arnoux, 5-Oct-2020)

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

Hypotheses | breq1d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

breqdi.1 | $${\u22a2}{\phi}\to {C}{A}{D}$$ | ||

Assertion | breqdi | $${\u22a2}{\phi}\to {C}{B}{D}$$ |

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

1 | breq1d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

2 | breqdi.1 | $${\u22a2}{\phi}\to {C}{A}{D}$$ | |

3 | 1 | breqd | $${\u22a2}{\phi}\to \left({C}{A}{D}\leftrightarrow {C}{B}{D}\right)$$ |

4 | 2 3 | mpbid | $${\u22a2}{\phi}\to {C}{B}{D}$$ |