Theorem breqd 5100

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   class class class wbr 5089

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-br 5090

This theorem is referenced by:  breq123d  5103  breqdi  5104  sbcbr123  5143  sbcbr  5144  sbcbr12g  5145  fvmptopab  7401  brfvopab  7403  mptmpoopabbrd  8012  mptmpoopabbrdOLD  8013  mptmpoopabovd  8014  bropopvvv  8020  bropfvvvvlem  8021  sprmpod  8154  fprlem1  8230  supeq123d  9334  frrlem15  9650  fpwwe2lem11  10532  fpwwe2  10534  brtrclfv  14909  dfrtrclrec2  14965  rtrclreclem3  14967  relexpindlem  14970  shftfib  14979  2shfti  14987  prdsval  17359  pwsle  17396  pwsleval  17397  imasleval  17445  issect  17660  isinv  17667  brcic  17705  ciclcl  17709  cicrcl  17710  isfunc  17771  funcres2c  17810  isfull  17819  isfth  17823  fullpropd  17829  fthpropd  17830  elhoma  17939  isposd  18228  pltval  18236  lubfval  18254  glbfval  18267  joinfval  18277  meetfval  18291  odujoin  18312  odumeet  18314  resstos  18336  ipole  18440  eqgval  19089  isomnd  20035  submomnd  20044  ogrpaddltrd  20052  unitpropd  20335  rngcifuestrc  20554  isorng  20776  znleval  21491  ltbval  21978  opsrval  21981  lmbr  23173  metustexhalf  24471  metucn  24486  isphtpc  24920  taylthlem1  26308  ulmval  26316  tgjustf  28451  iscgrg  28490  legov  28563  ishlg  28580  opphllem5  28729  opphllem6  28730  hpgbr  28738  iscgra  28787  acopy  28811  isinag  28816  isleag  28825  iseqlg  28845  wlkonprop  29635  wksonproplem  29681  istrlson  29683  upgrwlkdvspth  29717  ispthson  29720  isspthson  29721  cyclispthon  29782  wspthsn  29826  wspthsnon  29830  iswspthsnon  29834  1pthon2v  30133  3wlkond  30151  dfconngr1  30168  isconngr  30169  isconngr1  30170  1conngr  30174  conngrv2edg  30175  minvecolem4b  30858  minvecolem4  30860  br8d  32591  ressprs  32947  mntoval  32963  mgcoval  32967  mgcval  32968  isinftm  33150  rprmval  33481  metidv  33905  pstmfval  33909  faeval  34259  brfae  34261  isacycgr  35189  isacycgr1  35190  issconn  35270  satfbrsuc  35410  mclsax  35613  weiunpo  36509  weiunfr  36511  bj-imdirval3  37228  unceq  37636  alrmomodm  38390  relbrcoss  38547  lcvbr  39119  isopos  39278  cmtvalN  39309  isoml  39336  cvrfval  39366  cvrval  39367  pats  39383  isatl  39397  iscvlat  39421  ishlat1  39450  llnset  39603  lplnset  39627  lvolset  39670  lineset  39836  psubspset  39842  pmapfval  39854  lautset  40180  ldilfset  40206  ltrnfset  40215  trlfset  40258  diaffval  41128  dicffval  41272  dihffval  41328  prjspnvs  42712  fnwe2lem2  43143  fnwe2lem3  43144  aomclem8  43153  brfvid  43779  brfvidRP  43780  brfvrcld  43783  brfvrcld2  43784  iunrelexpuztr  43811  brtrclfv2  43819  neicvgnvor  44208  neicvgel1  44211  fperdvper  46016  upwlkbprop  48237  isprsd  49054  lubeldm2d  49057  glbeldm2d  49058  catprsc  49113  catprsc2  49114  oppccicb  49151  funcoppc2  49243  uptpos  49298  prsthinc  49564  prstcle  49656  lanup  49741  ranup  49742  islmd  49765  cmddu  49768  lmdran  49771  cmdlan  49772