Theorem breqd 5113

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5103

This theorem is referenced by:  breq123d  5116  breqdi  5117  sbcbr123  5156  sbcbr  5157  sbcbr12g  5158  fvmptopab  7424  brfvopab  7426  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  mptmpoopabovd  8040  bropopvvv  8046  bropfvvvvlem  8047  sprmpod  8180  fprlem1  8256  supeq123d  9377  frrlem15  9688  fpwwe2lem11  10572  fpwwe2  10574  brtrclfv  14945  dfrtrclrec2  15001  rtrclreclem3  15003  relexpindlem  15006  shftfib  15015  2shfti  15023  prdsval  17395  pwsle  17432  pwsleval  17433  imasleval  17481  issect  17696  isinv  17703  brcic  17741  ciclcl  17745  cicrcl  17746  isfunc  17807  funcres2c  17846  isfull  17855  isfth  17859  fullpropd  17865  fthpropd  17866  elhoma  17975  isposd  18264  pltval  18272  lubfval  18290  glbfval  18303  joinfval  18313  meetfval  18327  odujoin  18348  odumeet  18350  resstos  18372  ipole  18476  eqgval  19092  isomnd  20038  submomnd  20047  ogrpaddltrd  20055  unitpropd  20338  rngcifuestrc  20560  isorng  20782  znleval  21497  ltbval  21984  opsrval  21987  lmbr  23179  metustexhalf  24478  metucn  24493  isphtpc  24927  taylthlem1  26315  ulmval  26323  tgjustf  28454  iscgrg  28493  legov  28566  ishlg  28583  opphllem5  28732  opphllem6  28733  hpgbr  28741  iscgra  28790  acopy  28814  isinag  28819  isleag  28828  iseqlg  28848  wlkonprop  29638  wksonproplem  29684  istrlson  29686  upgrwlkdvspth  29720  ispthson  29723  isspthson  29724  cyclispthon  29785  wspthsn  29829  wspthsnon  29833  iswspthsnon  29837  1pthon2v  30133  3wlkond  30151  dfconngr1  30168  isconngr  30169  isconngr1  30170  1conngr  30174  conngrv2edg  30175  minvecolem4b  30858  minvecolem4  30860  br8d  32589  ressprs  32939  mntoval  32955  mgcoval  32959  mgcval  32960  isinftm  33151  rprmval  33481  metidv  33876  pstmfval  33880  faeval  34230  brfae  34232  isacycgr  35126  isacycgr1  35127  issconn  35207  satfbrsuc  35347  mclsax  35550  weiunpo  36447  weiunfr  36449  bj-imdirval3  37166  unceq  37585  alrmomodm  38335  relbrcoss  38431  lcvbr  39008  isopos  39167  cmtvalN  39198  isoml  39225  cvrfval  39255  cvrval  39256  pats  39272  isatl  39286  iscvlat  39310  ishlat1  39339  llnset  39493  lplnset  39517  lvolset  39560  lineset  39726  psubspset  39732  pmapfval  39744  lautset  40070  ldilfset  40096  ltrnfset  40105  trlfset  40148  diaffval  41018  dicffval  41162  dihffval  41218  prjspnvs  42602  fnwe2lem2  43034  fnwe2lem3  43035  aomclem8  43044  brfvid  43670  brfvidRP  43671  brfvrcld  43674  brfvrcld2  43675  iunrelexpuztr  43702  brtrclfv2  43710  neicvgnvor  44099  neicvgel1  44102  fperdvper  45911  upwlkbprop  48120  isprsd  48937  lubeldm2d  48940  glbeldm2d  48941  catprsc  48996  catprsc2  48997  oppccicb  49034  funcoppc2  49126  uptpos  49181  prsthinc  49447  prstcle  49539  lanup  49624  ranup  49625  islmd  49648  cmddu  49651  lmdran  49654  cmdlan  49655