Theorem breqdi 5122

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-br 5108

This theorem is used by:  rtrclreclem3  15135  episect  17878  dvef  26209  zerocgra  29208  acopyeu  29219  perpeqlem  29224  tgaaddcpbllem1  29226  tgaaddcpbllem2  29227  tgaaddcpbl  29229  tgaaddcpbl2  29230  isleagd  29244  angmndaddeu1  29252  angmndaddeu2  29253  angmndaddeu3  29254  angmndaddeu4  29255  angmndaddeu5  29256  angmndaddeu6  29257  angmndaddeu7  29258  angmndaddov2lem  29260  angmndaddcpbl  29263  weiunso  37072  0prjspn  43461  brfvimex  44853  brovmptimex  44854  ntrclsnvobr  44879  clsneibex  44929  neicvgbex  44939  up1st2nd  50098  up1st2ndr  50099