Theorem breqd 5121

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 5112	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-br 5111

This theorem is referenced by:  breq123d  5124  breqdi  5125  sbcbr123  5164  sbcbr  5165  sbcbr12g  5166  fvmptopab  7416  fvmptopabOLD  7417  brfvopab  7419  mptmpoopabbrd  8018  mptmpoopabovd  8019  mptmpoopabbrdOLD  8020  mptmpoopabovdOLD  8021  bropopvvv  8027  bropfvvvvlem  8028  sprmpod  8160  fprlem1  8236  wfrlem5OLD  8264  supeq123d  9395  frrlem15  9702  fpwwe2lem11  10586  fpwwe2  10588  brtrclfv  14899  dfrtrclrec2  14955  rtrclreclem3  14957  relexpindlem  14960  shftfib  14969  2shfti  14977  prdsval  17351  pwsle  17388  pwsleval  17389  imasleval  17437  issect  17650  isinv  17657  brcic  17695  ciclcl  17699  cicrcl  17700  isfunc  17764  funcres2c  17802  isfull  17811  isfth  17815  fullpropd  17821  fthpropd  17822  elhoma  17932  isposd  18226  pltval  18235  lubfval  18253  glbfval  18266  joinfval  18276  meetfval  18290  odujoin  18311  odumeet  18313  ipole  18437  eqgval  18993  unitpropd  20142  znleval  20998  ltbval  21481  opsrval  21484  lmbr  22646  metustexhalf  23949  metucn  23964  isphtpc  24394  taylthlem1  25769  ulmval  25776  tgjustf  27478  iscgrg  27517  legov  27590  ishlg  27607  opphllem5  27756  opphllem6  27757  hpgbr  27765  iscgra  27814  acopy  27838  isinag  27843  isleag  27852  iseqlg  27872  wlkonprop  28669  wksonproplem  28715  wksonproplemOLD  28716  istrlson  28718  upgrwlkdvspth  28750  ispthson  28753  isspthson  28754  cyclispthon  28812  wspthsn  28856  wspthsnon  28860  iswspthsnon  28864  1pthon2v  29160  3wlkond  29178  dfconngr1  29195  isconngr  29196  isconngr1  29197  1conngr  29201  conngrv2edg  29202  minvecolem4b  29883  minvecolem4  29885  br8d  31596  ressprs  31893  resstos  31897  mntoval  31912  mgcoval  31916  mgcval  31917  isomnd  31979  submomnd  31988  ogrpaddltrd  31997  isinftm  32087  isorng  32165  rprmval  32337  metidv  32562  pstmfval  32566  faeval  32934  brfae  32936  isacycgr  33826  isacycgr1  33827  issconn  33907  satfbrsuc  34047  mclsax  34250  bj-imdirval3  35728  unceq  36128  alrmomodm  36893  relbrcoss  36981  lcvbr  37556  isopos  37715  cmtvalN  37746  isoml  37773  cvrfval  37803  cvrval  37804  pats  37820  isatl  37834  iscvlat  37858  ishlat1  37887  llnset  38041  lplnset  38065  lvolset  38108  lineset  38274  psubspset  38280  pmapfval  38292  lautset  38618  ldilfset  38644  ltrnfset  38653  trlfset  38696  diaffval  39566  dicffval  39710  dihffval  39766  prjspnvs  41016  fnwe2lem2  41436  fnwe2lem3  41437  aomclem8  41446  brfvid  42081  brfvidRP  42082  brfvrcld  42085  brfvrcld2  42086  iunrelexpuztr  42113  brtrclfv2  42121  neicvgnvor  42510  neicvgel1  42513  fperdvper  44280  upwlkbprop  46160  rngcifuestrc  46415  isprsd  47108  lubeldm2d  47111  glbeldm2d  47112  catprsc  47153  catprsc2  47154  prsthinc  47194  prstcle  47210