Theorem breqd 5159

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809  df-br 5149

This theorem is referenced by:  breq123d  5162  breqdi  5163  sbcbr123  5202  sbcbr  5203  sbcbr12g  5204  fvmptopab  7466  fvmptopabOLD  7467  brfvopab  7469  mptmpoopabbrd  8071  mptmpoopabbrdOLD  8072  mptmpoopabovd  8073  mptmpoopabbrdOLDOLD  8074  mptmpoopabovdOLD  8075  bropopvvv  8081  bropfvvvvlem  8082  sprmpod  8215  fprlem1  8291  wfrlem5OLD  8319  supeq123d  9451  frrlem15  9758  fpwwe2lem11  10642  fpwwe2  10644  brtrclfv  14956  dfrtrclrec2  15012  rtrclreclem3  15014  relexpindlem  15017  shftfib  15026  2shfti  15034  prdsval  17408  pwsle  17445  pwsleval  17446  imasleval  17494  issect  17707  isinv  17714  brcic  17752  ciclcl  17756  cicrcl  17757  isfunc  17821  funcres2c  17861  isfull  17870  isfth  17874  fullpropd  17880  fthpropd  17881  elhoma  17992  isposd  18286  pltval  18295  lubfval  18313  glbfval  18326  joinfval  18336  meetfval  18350  odujoin  18371  odumeet  18373  ipole  18497  eqgval  19100  unitpropd  20315  rngcifuestrc  20531  znleval  21420  ltbval  21909  opsrval  21912  lmbr  23082  metustexhalf  24385  metucn  24400  isphtpc  24840  taylthlem1  26224  ulmval  26231  tgjustf  28158  iscgrg  28197  legov  28270  ishlg  28287  opphllem5  28436  opphllem6  28437  hpgbr  28445  iscgra  28494  acopy  28518  isinag  28523  isleag  28532  iseqlg  28552  wlkonprop  29349  wksonproplem  29395  wksonproplemOLD  29396  istrlson  29398  upgrwlkdvspth  29430  ispthson  29433  isspthson  29434  cyclispthon  29492  wspthsn  29536  wspthsnon  29540  iswspthsnon  29544  1pthon2v  29840  3wlkond  29858  dfconngr1  29875  isconngr  29876  isconngr1  29877  1conngr  29881  conngrv2edg  29882  minvecolem4b  30565  minvecolem4  30567  br8d  32273  ressprs  32567  resstos  32571  mntoval  32586  mgcoval  32590  mgcval  32591  isomnd  32656  submomnd  32665  ogrpaddltrd  32674  isinftm  32764  isorng  32854  rprmval  33074  metidv  33337  pstmfval  33341  faeval  33709  brfae  33711  isacycgr  34601  isacycgr1  34602  issconn  34682  satfbrsuc  34822  mclsax  35025  bj-imdirval3  36531  unceq  36931  alrmomodm  37694  relbrcoss  37782  lcvbr  38357  isopos  38516  cmtvalN  38547  isoml  38574  cvrfval  38604  cvrval  38605  pats  38621  isatl  38635  iscvlat  38659  ishlat1  38688  llnset  38842  lplnset  38866  lvolset  38909  lineset  39075  psubspset  39081  pmapfval  39093  lautset  39419  ldilfset  39445  ltrnfset  39454  trlfset  39497  diaffval  40367  dicffval  40511  dihffval  40567  prjspnvs  41827  fnwe2lem2  42258  fnwe2lem3  42259  aomclem8  42268  brfvid  42903  brfvidRP  42904  brfvrcld  42907  brfvrcld2  42908  iunrelexpuztr  42935  brtrclfv2  42943  neicvgnvor  43332  neicvgel1  43335  fperdvper  45096  upwlkbprop  46977  isprsd  47752  lubeldm2d  47755  glbeldm2d  47756  catprsc  47797  catprsc2  47798  prsthinc  47838  prstcle  47854