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 1570   class class class wbr 5102

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 2732

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

This theorem is used by:  rtrclreclem3  15180  episect  17921  dvef  26261  zerocgra  29264  acopyeu  29275  perpeqlem  29280  tgaaddcpbllem1  29282  tgaaddcpbllem2  29283  tgaaddcpbl  29285  tgaaddcpbl2  29286  isleagd  29300  cgraer  29310  cgrabasimass  29311  angmgmaddeu1  29312  angmgmaddeu2  29313  angmgmaddeu3  29314  angmgmaddeu4  29315  angmgmaddeu5  29316  angmgmaddeu6  29317  angmgmaddeu7  29318  angmgmaddov2lem  29320  angmgmaddcpbl  29323  angmgmaddlid  29325  angmgmaddrid  29326  weiunso  37176  0prjspn  43578  brfvimex  44970  brovmptimex  44971  ntrclsnvobr  44996  clsneibex  45046  neicvgbex  45056  up1st2nd  50215  up1st2ndr  50216