Theorem breqd 4588

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)

Hypothesis

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

Assertion

Ref	Expression
breqd	⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Proof of Theorem breqd

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq 4579	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ↔ wb 194   = wceq 1474   class class class wbr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605  df-br 4578

This theorem is referenced by:  breq123d  4591  breqdi  4592  sbcbr123  4630  sbcbr  4631  sbcbr12g  4632  fvmptopab1  6571  brfvopab  6575  bropopvvv  7119  bropfvvvvlem  7120  sprmpt2d  7214  wfrlem5  7283  supeq123d  8216  fpwwe2lem12  9319  fpwwe2  9321  brtrclfv  13539  dfrtrclrec2  13593  rtrclreclem3  13596  relexpindlem  13599  shftfib  13608  2shfti  13616  prdsval  15886  pwsle  15923  pwsleval  15924  imasleval  15972  issect  16184  isinv  16191  episect  16216  brcic  16229  ciclcl  16233  cicrcl  16234  isfunc  16295  funcres2c  16332  isfull  16341  isfth  16345  fullpropd  16351  fthpropd  16352  elhoma  16453  isposd  16726  pltval  16731  lubfval  16749  glbfval  16762  joinfval  16772  meetfval  16786  odumeet  16911  odujoin  16913  ipole  16929  eqgval  17414  unitpropd  18468  ltbval  19240  opsrval  19243  znleval  19669  lmbr  20819  metustexhalf  22118  metucn  22133  isphtpc  22548  dvef  23491  taylthlem1  23875  ulmval  23882  iscgrg  25152  legov  25225  ishlg  25242  opphllem5  25388  opphllem6  25389  hpgbr  25397  iscgra  25446  acopy  25469  acopyeu  25470  isinag  25474  isleag  25478  iseqlg  25492  wlkon  25854  iswlkon  25855  wlkonprop  25856  trls  25859  trlon  25863  istrlon  25864  trlonprop  25865  pths  25889  spths  25890  pthon  25898  ispthon  25899  pthonprop  25900  spthon  25905  isspthon  25906  spthonprp  25908  cyclispthon  25954  dfconngra1  25992  isconngra  25993  isconngra1  25994  1conngra  25996  clwlk  26074  clwlkcompim  26085  is2wlkonot  26183  is2spthonot  26184  2wlkonot  26185  2spthonot  26186  2wlkonot3v  26195  2spthonot3v  26196  iseupa  26285  minvecolem4b  26911  minvecolem4  26913  br8d  28595  ressprs  28779  resstos  28784  isomnd  28825  submomnd  28834  ogrpaddltrd  28844  isinftm  28859  isorng  28923  metidv  29056  pstmfval  29060  faeval  29429  brfae  29431  isscon  30255  mclsax  30513  frrlem5  30821  unceq  32339  lcvbr  33109  isopos  33268  cmtvalN  33299  isoml  33326  cvrfval  33356  cvrval  33357  pats  33373  isatl  33387  iscvlat  33411  ishlat1  33440  llnset  33592  lplnset  33616  lvolset  33659  lineset  33825  psubspset  33831  pmapfval  33843  lautset  34169  ldilfset  34195  ltrnfset  34204  trlfset  34248  diaffval  35120  dicffval  35264  dihffval  35320  fnwe2lem2  36422  fnwe2lem3  36423  aomclem8  36432  brfvid  36781  brfvidRP  36782  brfvrcld  36785  brfvrcld2  36786  iunrelexpuztr  36813  brtrclfv2  36821  neicvgnvor  37217  neicvgel1  37220  fperdvper  38591  mptmpt2opabbrd  40141  mptmpt2opabovd  40142  wlkbProp  40798  wlkOnprop  40847  1wlksonproplem  40893  istrlson  40895  upgrwlkdvspth  40926  ispthson  40929  isspthson  40930  cyclisPthon  40988  wspthsn  41027  wspthsnon  41031  iswspthsnon  41033  1pthon2v-av  41301  31wlkond  41319  dfconngr1  41336  isconngr  41337  isconngr1  41338  1conngr  41342  conngrv2edg  41343  rngcifuestrc  41770