Theorem breqdi 5117

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 5113	. 2 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
4	1, 3	mpbid 235	1 ⊢ (𝜑 → 𝐶𝐵𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-br 5103

This theorem is used by:  rtrclreclem3  15213  episect  17960  dvef  26300  zerocgra  29331  acopyeu  29342  perpeqlem  29347  tgaaddcpbllem1  29349  tgaaddcpbllem2  29350  tgaaddcpbl  29352  tgaaddcpbl2  29353  isleagd  29367  cgraer  29377  cgrabasimass  29378  angmgmaddeu1  29379  angmgmaddeu2  29380  angmgmaddeu3  29381  angmgmaddeu4  29382  angmgmaddeu5  29383  angmgmaddeu6  29384  angmgmaddeu7  29385  angmgmaddov2lem  29387  angmgmaddcpbl  29390  angmgmaddlid  29392  angmgmaddrid  29393  weiunso  37254  0prjspn  43665  brfvimex  45026  brovmptimex  45027  ntrclsnvobr  45052  clsneibex  45102  neicvgbex  45112  up1st2nd  50293  up1st2ndr  50294