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  9686  fpwwe2lem11  10570  fpwwe2  10572  brtrclfv  14944  dfrtrclrec2  15000  rtrclreclem3  15002  relexpindlem  15005  shftfib  15014  2shfti  15022  prdsval  17394  pwsle  17431  pwsleval  17432  imasleval  17480  issect  17695  isinv  17702  brcic  17740  ciclcl  17744  cicrcl  17745  isfunc  17806  funcres2c  17845  isfull  17854  isfth  17858  fullpropd  17864  fthpropd  17865  elhoma  17974  isposd  18263  pltval  18271  lubfval  18289  glbfval  18302  joinfval  18312  meetfval  18326  odujoin  18347  odumeet  18349  resstos  18371  ipole  18475  eqgval  19091  isomnd  20037  submomnd  20046  ogrpaddltrd  20054  unitpropd  20337  rngcifuestrc  20559  isorng  20781  znleval  21496  ltbval  21983  opsrval  21986  lmbr  23178  metustexhalf  24477  metucn  24492  isphtpc  24926  taylthlem1  26314  ulmval  26322  tgjustf  28453  iscgrg  28492  legov  28565  ishlg  28582  opphllem5  28731  opphllem6  28732  hpgbr  28740  iscgra  28789  acopy  28813  isinag  28818  isleag  28827  iseqlg  28847  wlkonprop  29637  wksonproplem  29683  istrlson  29685  upgrwlkdvspth  29719  ispthson  29722  isspthson  29723  cyclispthon  29784  wspthsn  29828  wspthsnon  29832  iswspthsnon  29836  1pthon2v  30132  3wlkond  30150  dfconngr1  30167  isconngr  30168  isconngr1  30169  1conngr  30173  conngrv2edg  30174  minvecolem4b  30857  minvecolem4  30859  br8d  32588  ressprs  32938  mntoval  32954  mgcoval  32958  mgcval  32959  isinftm  33150  rprmval  33480  metidv  33875  pstmfval  33879  faeval  34229  brfae  34231  isacycgr  35125  isacycgr1  35126  issconn  35206  satfbrsuc  35346  mclsax  35549  weiunpo  36446  weiunfr  36448  bj-imdirval3  37165  unceq  37584  alrmomodm  38334  relbrcoss  38430  lcvbr  39007  isopos  39166  cmtvalN  39197  isoml  39224  cvrfval  39254  cvrval  39255  pats  39271  isatl  39285  iscvlat  39309  ishlat1  39338  llnset  39492  lplnset  39516  lvolset  39559  lineset  39725  psubspset  39731  pmapfval  39743  lautset  40069  ldilfset  40095  ltrnfset  40104  trlfset  40147  diaffval  41017  dicffval  41161  dihffval  41217  prjspnvs  42601  fnwe2lem2  43033  fnwe2lem3  43034  aomclem8  43043  brfvid  43669  brfvidRP  43670  brfvrcld  43673  brfvrcld2  43674  iunrelexpuztr  43701  brtrclfv2  43709  neicvgnvor  44098  neicvgel1  44101  fperdvper  45910  upwlkbprop  48119  isprsd  48936  lubeldm2d  48939  glbeldm2d  48940  catprsc  48995  catprsc2  48996  oppccicb  49033  funcoppc2  49125  uptpos  49180  prsthinc  49446  prstcle  49538  lanup  49623  ranup  49624  islmd  49647  cmddu  49650  lmdran  49653  cmdlan  49654