Theorem breqdi 5121

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

Hypotheses

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
breqdi.1	⊢ (𝜑 → 𝐶𝐴𝐷)

Assertion

Ref	Expression
breqdi	⊢ (𝜑 → 𝐶𝐵𝐷)

Proof of Theorem breqdi

Step	Hyp	Ref	Expression
1		breqdi.1	. 2 ⊢ (𝜑 → 𝐶𝐴𝐷)
2		breq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breqd 5117	. 2 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
4	1, 3	mpbid 235	1 ⊢ (𝜑 → 𝐶𝐵𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-br 5107

This theorem is used by:  rtrclreclem3  15239  episect  17986  dvef  26327  zerocgra  29358  acopyeu  29369  perpeqlem  29374  tgaaddcpbllem1  29376  tgaaddcpbllem2  29377  tgaaddcpbl  29379  tgaaddcpbl2  29380  isleagd  29394  cgraer  29404  cgrabasimass  29405  angmgmaddeu1  29406  angmgmaddeu2  29407  angmgmaddeu3  29408  angmgmaddeu4  29409  angmgmaddeu5  29410  angmgmaddeu6  29411  angmgmaddeu7  29412  angmgmaddov2lem  29414  angmgmaddcpbl  29417  angmgmaddlid  29419  angmgmaddrid  29420  weiunso  37431  0prjspn  43855  brfvimex  45216  brovmptimex  45217  ntrclsnvobr  45242  clsneibex  45292  neicvgbex  45302  up1st2nd  50504  up1st2ndr  50505