Theorem breqtrrd 5109

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrrd.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
breqtrrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2742	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 5107	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5081

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082

This theorem is referenced by:  marypha1lem  9236  marypha2  9242  infsupprpr  9307  unxpwdom  9392  ttrcltr  9518  onadju  9995  nnadju  9999  cfss  10067  tskuni  10585  ltexnq  10777  lt2addmuld  12269  div4p1lem1div2  12274  mul2lt0rgt0  12879  prodge0ld  12884  xrmax1  12955  xrmax2  12956  max1ALT  12966  qbtwnxr  12980  xleadd1a  13033  xlt2add  13040  xlesubadd  13043  xmulgt0  13063  xlemul1a  13068  xov1plusxeqvd  13276  uzsubsubfz  13324  fzctr  13414  subfzo0  13555  flflp1  13573  fldiv4lem1div2uz2  13602  ceilge  13611  modge0  13645  modlt  13646  modid  13662  m1modge3gt1  13684  modaddmodup  13700  sermono  13801  seqf1olem1  13808  seqf1olem2  13809  sqgt0  13891  sqge0  13901  leexp1a  13939  nnlesq  13968  expnbnd  13993  expmulnbnd  13996  discr1  14000  facwordi  14049  faclbnd5  14058  nfile  14119  hashdom  14139  hashgt23el  14184  fi1uzind  14256  brfi1indALT  14259  ccatws1n0  14387  swrds2  14698  cjmulge0  14902  resqrtcl  15010  absge0  15044  sqreulem  15116  amgm2  15126  rlimdm  15305  rlimge0  15335  reccn2  15351  climle  15394  climserle  15419  isercoll2  15425  iseraltlem1  15438  iseralt  15441  isumclim2  15515  isumclim3  15516  isumge0  15523  fsumless  15553  cvgcmp  15573  cvgcmpce  15575  abscvgcvg  15576  isumsup2  15603  isumltss  15605  climcndslem1  15606  climcnds  15608  supcvg  15613  harmonic  15616  expcnv  15621  explecnv  15622  cvgrat  15640  mertenslem1  15641  mertenslem2  15642  clim2div  15646  ntrivcvgtail  15657  iprodclim2  15754  iprodclim3  15755  efcvg  15839  ege2le3  15844  efaddlem  15847  eftlub  15863  effsumlt  15865  tanhlt1  15914  ef01bndlem  15938  sin02gt0  15946  rpnnen2lem4  15971  ruclem2  15986  ruclem3  15987  ruclem9  15992  iddvdsexp  16034  dvdsadd  16056  dvdsfac  16080  dvdsexp2im  16081  dvdsmod  16083  3dvds  16085  omoe  16118  sumeven  16141  divalglem1  16148  flodddiv4t2lthalf  16170  bitsfzo  16187  bitsmod  16188  bitscmp  16190  bitsinv1lem  16193  sadcaddlem  16209  sadadd3  16213  sadaddlem  16218  dvdssqim  16309  dvdsmulgcd  16310  nn0seqcvgd  16320  dvdslcm  16348  lcmgcdlem  16356  dvdslcmf  16381  lcmfunsnlem2lem2  16389  mulgcddvds  16405  qredeq  16407  cncongr2  16418  sqnprm  16452  isprm6  16464  nonsq  16508  hashdvds  16521  prmdiv  16531  odzdvds  16541  pythagtriplem4  16565  pcpre1  16588  pcdvdsb  16615  pcz  16627  pcprmpw2  16628  pcaddlem  16634  pcadd  16635  pcadd2  16636  pcmpt  16638  pcmptdvds  16640  fldivp1  16643  pcfaclem  16644  pockthlem  16651  prmreclem1  16662  prmreclem3  16664  prmreclem5  16666  prmreclem6  16667  4sqlem6  16689  4sqlem8  16691  4sqlem11  16701  4sqlem12  16702  4sqlem14  16704  4sqlem16  16706  vdwlem3  16729  vdwlem9  16735  vdwlem10  16736  vdwlem12  16738  ramub1lem2  16773  prmgap  16805  prmgaplcm  16806  prmgapprmo  16808  mreexexd  17402  invfuc  17737  ple1  18193  eqgen  18854  lagsubg  18863  pgpfi  19255  sylow2alem2  19268  sylow2a  19269  sylow3lem4  19280  efgsrel  19385  odadd1  19494  odadd2  19495  gexex  19499  lt6abl  19541  dprd2d2  19692  dmdprdpr  19697  ablfacrp2  19715  ablfac1c  19719  pgpfaclem1  19729  ablfac2  19737  fincygsubgodd  19760  dvdsrmul1  19940  unitmulclb  19952  subrguss  20084  abvres  20144  znfld  20813  znunit  20816  frlmisfrlm  21100  ply1coefsupp  21511  evl1gsumadd  21569  matgsum  21631  pm2mpcl  21991  psmetxrge0  23511  isxmet2d  23525  mettri  23550  xmettri3  23551  mettri3  23552  xmetrtri2  23554  prdsxmetlem  23566  imasdsf1olem  23571  xblss2ps  23599  blss2ps  23601  blss2  23602  blssps  23622  blss  23623  prdsbl  23692  dscmet  23773  nmge0  23818  nmmtri  23823  tngngp3  23865  nlmvscnlem2  23894  nrginvrcnlem  23900  nmoix  23938  nmoleub  23940  blcvx  24006  xrsxmet  24017  opnreen  24039  xrge0tsms  24042  icopnfcnv  24150  xrhmeo  24154  lebnumii  24174  pcophtb  24237  pi1grplem  24257  nmoleub2lem  24322  ipcau2  24443  tcphcphlem1  24444  ipcau  24447  ipcnlem2  24453  rrxcph  24601  minveclem2  24635  minveclem3b  24637  pjthlem1  24646  pjthlem2  24647  ivthlem3  24662  ivth2  24664  ovolfsf  24680  ovolsslem  24693  ovollb2lem  24697  ovollb2  24698  ovolctb  24699  ovolfiniun  24710  ovolicc1  24725  ovolicc2lem4  24729  ovolicc2  24731  nulmbl2  24745  unmbl  24746  ioombl1lem4  24770  uniioombllem4  24795  uniioombllem6  24797  volivth  24816  vitalilem4  24820  itg1ge0  24895  itg1ge0a  24921  itg1lea  24922  itg1climres  24924  mbfi1fseqlem5  24929  itg2ub  24943  itg2seq  24952  itg2uba  24953  itg2splitlem  24958  itg2split  24959  itg2monolem3  24962  itg2mono  24963  itg2i1fseq2  24966  itg2addlem  24968  iblss  25014  itggt0  25053  dvferm2lem  25195  dvlip  25202  dvivthlem1  25217  dvfsumlem2  25236  dvfsumlem3  25237  ftc1lem4  25248  ply1divmo  25345  ply1remlem  25372  fta1glem2  25376  ig1pdvds  25386  plyeq0lem  25416  plydiveu  25503  fta1lem  25512  vieta1lem2  25516  aaliou3lem2  25548  aaliou3lem8  25550  ulmcn  25603  mtest  25608  itgulm  25612  radcnvlem1  25617  radcnvlt1  25622  dvradcnv  25625  pserdvlem2  25632  abelthlem2  25636  abelthlem6  25640  abelthlem7  25642  abelthlem9  25644  tangtx  25707  sinq12gt0  25709  sineq0  25725  cosordlem  25731  tanord  25739  tanregt0  25740  logrnaddcl  25775  logcj  25806  argregt0  25810  argrege0  25811  argimgt0  25812  argimlt0  25813  logimul  25814  logneg2  25815  logdivlti  25820  divlogrlim  25835  logcnlem3  25844  logcnlem4  25845  dvlog2lem  25852  logtayl  25860  rpcxpcl  25876  cxpsqrtlem  25902  cxpaddle  25950  isosctrlem1  26013  asinlem3a  26065  asinlem3  26066  asinneg  26081  asinsinlem  26086  asinsin  26087  atanlogaddlem  26108  atanlogadd  26109  atanlogsublem  26110  atanlogsub  26111  atantan  26118  atanbndlem  26120  atantayl  26132  leibpi  26137  birthdaylem3  26148  areaf  26156  cxploglim  26172  jensenlem2  26182  jensen  26183  logdiflbnd  26189  harmonicbnd4  26205  fsumharmonic  26206  zetacvg  26209  lgamgulmlem2  26224  lgamgulmlem3  26225  lgamcvg2  26249  wilthlem2  26263  wilthimp  26266  ftalem1  26267  ftalem2  26268  ftalem5  26271  basellem6  26280  basellem8  26282  basellem9  26283  chtge0  26306  chtublem  26404  logexprlim  26418  perfectlem1  26422  bcmax  26471  bposlem1  26477  bposlem2  26478  bposlem6  26482  bposlem7  26483  lgsdilem2  26526  lgsqrlem4  26542  lgsquadlem1  26573  2lgsoddprmlem2  26602  2sqlem3  26613  2sqlem8  26619  2sqblem  26624  2sqmod  26629  chebbnd1lem2  26663  chtppilimlem1  26666  chtppilim  26668  chto1ub  26669  vmadivsum  26675  rplogsumlem1  26677  rplogsumlem2  26678  dchrisum0lem1a  26679  rpvmasumlem  26680  dchrisumlem1  26682  dchrisumlem2  26683  dchrvmasumlem2  26691  dchrisum0flblem1  26701  dchrisum0flblem2  26702  dchrisum0lem1b  26708  dchrisum0lem1  26709  dchrisum0lem2a  26710  dchrisum0lem3  26712  dchrisum0  26713  mudivsum  26723  mulogsumlem  26724  mulog2sumlem1  26727  mulog2sumlem2  26728  2vmadivsumlem  26733  chpdifbndlem1  26746  selberg3lem1  26750  selberg4lem1  26753  pntrlog2bndlem1  26770  pntrlog2bndlem2  26771  pntrlog2bndlem3  26772  pntrlog2bndlem4  26773  pntpbnd1a  26778  pntpbnd1  26779  pntpbnd2  26780  pntibndlem2  26784  pntibndlem3  26785  pntlemd  26787  pntlemc  26788  pntlemb  26790  pntlemg  26791  pntlemh  26792  pntlemr  26795  pntlemf  26798  pntlemo  26800  abvcxp  26808  ostth2lem1  26811  padicabv  26823  ostth2lem2  26827  ostth2lem3  26828  ostth2lem4  26829  ostth2  26830  ostth3  26831  tgcgr4  26937  legso  27005  krippenlem  27096  midex  27143  oppperpex  27159  ttgcontlem1  27297  axpaschlem  27353  axcontlem8  27384  upgrex  27507  nbfusgrlevtxm1  27789  finsumvtxdgeven  27964  wwlksnextproplem3  28321  clwlkclwwlk2  28412  clwlkclwwlkfolem  28416  clwwlkndivn  28489  ex-ind-dvds  28870  nvabs  29079  nmooge0  29174  nmoolb  29178  siii  29260  minvecolem2  29282  minvecolem4  29287  minvecolem5  29288  hlipgt0  29321  normge0  29533  normpyc  29553  pjhthlem1  29798  pjige0i  30097  nmoplb  30314  nmfnlb  30331  branmfn  30512  pjssdif2i  30581  stlei  30647  xlt2addrd  31126  eliccelico  31143  elicoelioo  31144  bcm1n  31161  dvdszzq  31174  prmdvdsbc  31175  fsumiunle  31188  pfxlsw2ccat  31269  wrdt2ind  31270  xrge0tsmsd  31362  omndmul2  31383  psgnfzto1stlem  31412  cycpmco2lem4  31441  cycpmco2lem5  31442  cyc3conja  31469  archirngz  31488  archiabllem2c  31494  ofldchr  31558  fedgmullem2  31756  extdggt0  31777  madjusmdetlem2  31823  locfinreflem  31835  xrge0iifiso  31930  nexple  32022  gsumesum  32072  esumcst  32076  esumpcvgval  32091  esumcvg  32099  esumiun  32107  measssd  32228  measunl  32229  omssubadd  32312  carsgclctunlem3  32332  pmeasmono  32336  sibfof  32352  oddpwdc  32366  eulerpartlemgc  32374  iwrdsplit  32399  ballotlemsgt1  32522  ballotlemsel1i  32524  sgnmul  32554  signsply0  32575  signstfvc  32598  signsvtp  32607  signsvfpn  32609  fdvposlt  32624  fdvneggt  32625  fdvnegge  32627  logdivsqrle  32675  hgt750lemf  32678  tgoldbachgtde  32685  swrdwlk  33133  subfaclim  33195  erdszelem7  33204  erdszelem8  33205  cvmliftlem2  33293  snmlff  33336  sinccvglem  33675  climlec3  33744  faclim  33757  nodense  33940  nogt01o  33944  nosupbnd2lem1  33963  noetasuplem3  33983  cofcutr  34137  cofcutrtime  34138  fnejoin1  34602  poimirlem12  35833  poimirlem17  35838  poimirlem19  35840  poimirlem20  35841  poimirlem23  35844  poimirlem28  35849  broucube  35855  mblfinlem2  35859  mblfinlem3  35860  mblfinlem4  35861  ismblfin  35862  itg2addnclem  35872  itg2addnclem3  35874  itg2gt0cn  35876  itggt0cn  35891  ftc1anclem5  35898  ftc1anclem7  35900  ftc1anclem8  35901  isbnd3  35986  ssbnd  35990  heiborlem8  36020  bfplem2  36025  rrncmslem  36034  rrnequiv  36037  rrntotbnd  36038  lcv1  37097  lsatcv0eq  37103  lsatcvat3  37108  cvlsupr2  37399  hlatlej2  37432  cvrval4N  37470  cvratlem  37477  atcvr0eq  37482  2atlt  37495  atbtwnex  37504  athgt  37512  1cvrat  37532  ps-1  37533  hlatexch3N  37536  hlatexch4  37537  3atlem2  37540  atcvrlln2  37575  lplnexllnN  37620  4atlem3a  37653  4atlem10b  37661  4atlem11b  37664  4atlem12b  37667  2lplnja  37675  dalemply  37710  dalemsly  37711  dalem1  37715  dalem6  37724  dalem7  37725  dalem-cly  37727  dalem11  37730  dalem12  37731  dalem16  37735  dalem17  37736  dalem38  37766  dalem44  37772  dalem61  37789  lnatexN  37835  lncvrat  37838  lncmp  37839  paddasslem2  37877  dalawlem3  37929  dalawlem6  37932  dalawlem11  37937  lhpmcvr  38079  lhp2atne  38090  lhp2at0ne  38092  lautj  38149  trlval4  38244  cdlemc2  38248  cdlemc5  38251  cdleme3b  38285  cdleme11c  38317  cdleme19a  38359  cdleme20j  38374  cdleme22f  38402  cdleme23c  38407  cdleme26f2ALTN  38420  cdleme26f2  38421  cdleme35fnpq  38505  cdleme48bw  38558  cdlemg10a  38696  cdlemg11b  38698  cdlemg17g  38723  cdlemg18c  38736  cdlemi1  38874  cdlemk52  39010  dia2dimlem1  39120  dihord1  39274  dihjatcclem4  39477  lcmineqlem15  40093  lcmineqlem19  40097  lcmineqlem22  40100  aks4d1lem1  40112  aks4d1p1p4  40121  aks4d1p1p5  40125  aks4d1p2  40127  aks4d1p3  40128  aks4d1p6  40131  aks4d1p7d1  40132  aks4d1p7  40133  aks4d1p8  40137  aks4d1p9  40138  sticksstones7  40150  metakunt7  40173  metakunt15  40181  metakunt16  40182  2xp3dxp2ge1d  40204  dvdsexpim  40365  dvdsexpnn0  40378  prjspner01  40499  flt4lem5  40524  fltnltalem  40536  fltnlta  40537  3cubeslem1  40543  eldioph2lem1  40619  lzenom  40629  irrapxlem1  40681  irrapxlem4  40684  irrapxlem5  40685  pell14qrgt0  40718  pell1qrge1  40729  pell1qrgap  40733  pellfundge  40741  pellfundex  40745  pellfund14  40757  rmspecsqrtnq  40765  rmxypos  40807  ltrmynn0  40808  ltrmxnn0  40809  jm2.24nn  40819  jm2.17b  40821  jm2.17c  40822  jm2.24  40823  congadd  40826  congsym  40828  congneg  40829  congid  40831  mzpcong  40832  acongrep  40840  acongeq  40843  jm2.18  40848  jm2.19  40853  jm2.23  40856  jm2.25  40859  jm2.26lem3  40861  jm2.15nn0  40863  jm2.16nn0  40864  jm2.27a  40865  jm2.27c  40867  jm3.1lem1  40877  idomrootle  41058  idomsubgmo  41061  sqrtcval  41287  inductionexd  41803  imo72b2  41821  dvgrat  41968  radcnvrat  41970  binomcxplemnn0  42005  binomcxplemnotnn0  42012  cncmpmax  42613  rnmptlb  42833  zltlesub  42872  infxrpnf  43034  xrpnf  43074  fmul01  43170  fmul01lt1lem1  43174  climdivf  43202  sumnnodd  43220  climinf2lem  43296  limsup10exlem  43362  climliminf  43396  dfxlim2v  43437  xlimliminflimsup  43452  dvdivbd  43513  volge0  43551  stoweidlem1  43591  stoweidlem16  43606  stoweidlem18  43608  stoweidlem24  43614  stoweidlem26  43616  stoweidlem36  43626  stoweidlem38  43628  stoweidlem41  43631  stoweidlem42  43632  stoweidlem44  43634  stoweidlem45  43635  stoweidlem48  43638  stoweidlem62  43652  wallispilem5  43659  stirlinglem1  43664  stirlinglem5  43668  stirlinglem7  43670  stirlinglem8  43671  stirlinglem9  43672  stirlinglem11  43674  fourierdlem4  43701  fourierdlem10  43707  fourierdlem37  43734  fourierdlem47  43743  fourierdlem72  43768  fourierdlem74  43770  fourierdlem79  43775  fourierdlem82  43778  fourierdlem89  43785  fourierdlem91  43787  fourierdlem93  43789  fourierdlem103  43799  fourierdlem104  43800  fourierdlem112  43808  etransclem24  43848  etransclem25  43849  etransclem28  43852  etransclem37  43861  etransclem38  43862  etransclem44  43868  meaiuninc3v  44072  vonicclem1  44271  pimconstlt0  44289  smfsuplem1  44398  rlimdmafv  44727  rlimdmafv2  44808  2elfz2melfz  44868  iccpartgtprec  44930  iccpartlt  44934  iccpartgtl  44936  sqrtpwpw2p  45048  fmtnodvds  45054  goldbachthlem1  45055  lighneallem4a  45118  perfectALTVlem1  45231  cznnring  45572  rhmsubcrngc  45645  altgsumbcALT  45747  expnegico01  45917  flnn0div2ge  45937  rege1logbrege0  45962  fllogbd  45964  nnpw2blen  45984  nnolog2flm1  45994  dignn0ldlem  46006  dignn0flhalflem1  46019  dignn0flhalflem2  46020  eenglngeehlnmlem2  46142  itsclc0yqsol  46168  2itscp  46185  itscnhlinecirc02plem1  46186  itscnhlinecirc02plem2  46187  inlinecirc02p  46191