Theorem breqtrrd 5138

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 2737	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 5136	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  marypha1lem  9378  marypha2  9384  infsupprpr  9449  unxpwdom  9534  ttrcltr  9661  onadju  10138  nnadju  10142  cfss  10210  tskuni  10728  ltexnq  10920  lt2addmuld  12412  div4p1lem1div2  12417  mul2lt0rgt0  13027  prodge0ld  13032  xrmax1  13104  xrmax2  13105  max1ALT  13115  qbtwnxr  13129  xleadd1a  13182  xlt2add  13189  xlesubadd  13192  xmulgt0  13212  xlemul1a  13217  xov1plusxeqvd  13425  uzsubsubfz  13473  fzctr  13563  subfzo0  13704  flflp1  13722  fldiv4lem1div2uz2  13751  ceilge  13760  modge0  13794  modlt  13795  modid  13811  m1modge3gt1  13833  modaddmodup  13849  sermono  13950  seqf1olem1  13957  seqf1olem2  13958  sqgt0  14041  sqge0  14051  leexp1a  14090  nnlesq  14119  expnbnd  14145  expmulnbnd  14148  discr1  14152  facwordi  14199  faclbnd5  14208  nfile  14269  hashdom  14289  hashgt23el  14334  fi1uzind  14408  brfi1indALT  14411  ccatws1n0  14532  swrds2  14841  cjmulge0  15043  resqrtcl  15150  absge0  15184  sqreulem  15256  amgm2  15266  rlimdm  15445  rlimge0  15475  reccn2  15491  climle  15534  climserle  15559  isercoll2  15565  iseraltlem1  15578  iseralt  15581  isumclim2  15654  isumclim3  15655  isumge0  15662  fsumless  15692  cvgcmp  15712  cvgcmpce  15714  abscvgcvg  15715  isumsup2  15742  isumltss  15744  climcndslem1  15745  climcnds  15747  supcvg  15752  harmonic  15755  expcnv  15760  explecnv  15761  cvgrat  15779  mertenslem1  15780  mertenslem2  15781  clim2div  15785  ntrivcvgtail  15796  iprodclim2  15893  iprodclim3  15894  efcvg  15978  ege2le3  15983  efaddlem  15986  eftlub  16002  effsumlt  16004  tanhlt1  16053  ef01bndlem  16077  sin02gt0  16085  rpnnen2lem4  16110  ruclem2  16125  ruclem3  16126  ruclem9  16131  iddvdsexp  16173  dvdsadd  16195  dvdsfac  16219  dvdsexp2im  16220  dvdsmod  16222  3dvds  16224  omoe  16257  sumeven  16280  divalglem1  16287  flodddiv4t2lthalf  16309  bitsfzo  16326  bitsmod  16327  bitscmp  16329  bitsinv1lem  16332  sadcaddlem  16348  sadadd3  16352  sadaddlem  16357  dvdssqim  16446  dvdsmulgcd  16447  nn0seqcvgd  16457  dvdslcm  16485  lcmgcdlem  16493  dvdslcmf  16518  lcmfunsnlem2lem2  16526  mulgcddvds  16542  qredeq  16544  cncongr2  16555  sqnprm  16589  isprm6  16601  nonsq  16645  hashdvds  16658  prmdiv  16668  odzdvds  16678  pythagtriplem4  16702  pcpre1  16725  pcdvdsb  16752  pcz  16764  pcprmpw2  16765  pcaddlem  16771  pcadd  16772  pcadd2  16773  pcmpt  16775  pcmptdvds  16777  fldivp1  16780  pcfaclem  16781  pockthlem  16788  prmreclem1  16799  prmreclem3  16801  prmreclem5  16803  prmreclem6  16804  4sqlem6  16826  4sqlem8  16828  4sqlem11  16838  4sqlem12  16839  4sqlem14  16841  4sqlem16  16843  vdwlem3  16866  vdwlem9  16872  vdwlem10  16873  vdwlem12  16875  ramub1lem2  16910  prmgap  16942  prmgaplcm  16943  prmgapprmo  16945  mreexexd  17542  invfuc  17877  ple1  18333  eqgen  18997  lagsubg  19006  pgpfi  19401  sylow2alem2  19414  sylow2a  19415  sylow3lem4  19426  efgsrel  19530  odadd1  19640  odadd2  19641  gexex  19645  lt6abl  19686  dprd2d2  19837  dmdprdpr  19842  ablfacrp2  19860  ablfac1c  19864  pgpfaclem1  19874  ablfac2  19882  fincygsubgodd  19905  dvdsrmul1  20096  unitmulclb  20108  subrguss  20285  abvres  20354  znfld  21004  znunit  21007  frlmisfrlm  21291  ply1coefsupp  21703  evl1gsumadd  21761  matgsum  21823  pm2mpcl  22183  psmetxrge0  23703  isxmet2d  23717  mettri  23742  xmettri3  23743  mettri3  23744  xmetrtri2  23746  prdsxmetlem  23758  imasdsf1olem  23763  xblss2ps  23791  blss2ps  23793  blss2  23794  blssps  23814  blss  23815  prdsbl  23884  dscmet  23965  nmge0  24010  nmmtri  24015  tngngp3  24057  nlmvscnlem2  24086  nrginvrcnlem  24092  nmoix  24130  nmoleub  24132  blcvx  24198  xrsxmet  24209  opnreen  24231  xrge0tsms  24234  icopnfcnv  24342  xrhmeo  24346  lebnumii  24366  pcophtb  24429  pi1grplem  24449  nmoleub2lem  24514  ipcau2  24635  tcphcphlem1  24636  ipcau  24639  ipcnlem2  24645  rrxcph  24793  minveclem2  24827  minveclem3b  24829  pjthlem1  24838  pjthlem2  24839  ivthlem3  24854  ivth2  24856  ovolfsf  24872  ovolsslem  24885  ovollb2lem  24889  ovollb2  24890  ovolctb  24891  ovolfiniun  24902  ovolicc1  24917  ovolicc2lem4  24921  ovolicc2  24923  nulmbl2  24937  unmbl  24938  ioombl1lem4  24962  uniioombllem4  24987  uniioombllem6  24989  volivth  25008  vitalilem4  25012  itg1ge0  25087  itg1ge0a  25113  itg1lea  25114  itg1climres  25116  mbfi1fseqlem5  25121  itg2ub  25135  itg2seq  25144  itg2uba  25145  itg2splitlem  25150  itg2split  25151  itg2monolem3  25154  itg2mono  25155  itg2i1fseq2  25158  itg2addlem  25160  iblss  25206  itggt0  25245  dvferm2lem  25387  dvlip  25394  dvivthlem1  25409  dvfsumlem2  25428  dvfsumlem3  25429  ftc1lem4  25440  ply1divmo  25537  ply1remlem  25564  fta1glem2  25568  ig1pdvds  25578  plyeq0lem  25608  plydiveu  25695  fta1lem  25704  vieta1lem2  25708  aaliou3lem2  25740  aaliou3lem8  25742  ulmcn  25795  mtest  25800  itgulm  25804  radcnvlem1  25809  radcnvlt1  25814  dvradcnv  25817  pserdvlem2  25824  abelthlem2  25828  abelthlem6  25832  abelthlem7  25834  abelthlem9  25836  tangtx  25899  sinq12gt0  25901  sineq0  25917  cosordlem  25923  tanord  25931  tanregt0  25932  logrnaddcl  25967  logcj  25998  argregt0  26002  argrege0  26003  argimgt0  26004  argimlt0  26005  logimul  26006  logneg2  26007  logdivlti  26012  divlogrlim  26027  logcnlem3  26036  logcnlem4  26037  dvlog2lem  26044  logtayl  26052  rpcxpcl  26068  cxpsqrtlem  26094  cxpaddle  26142  isosctrlem1  26205  asinlem3a  26257  asinlem3  26258  asinneg  26273  asinsinlem  26278  asinsin  26279  atanlogaddlem  26300  atanlogadd  26301  atanlogsublem  26302  atanlogsub  26303  atantan  26310  atanbndlem  26312  atantayl  26324  leibpi  26329  birthdaylem3  26340  areaf  26348  cxploglim  26364  jensenlem2  26374  jensen  26375  logdiflbnd  26381  harmonicbnd4  26397  fsumharmonic  26398  zetacvg  26401  lgamgulmlem2  26416  lgamgulmlem3  26417  lgamcvg2  26441  wilthlem2  26455  wilthimp  26458  ftalem1  26459  ftalem2  26460  ftalem5  26463  basellem6  26472  basellem8  26474  basellem9  26475  chtge0  26498  chtublem  26596  logexprlim  26610  perfectlem1  26614  bcmax  26663  bposlem1  26669  bposlem2  26670  bposlem6  26674  bposlem7  26675  lgsdilem2  26718  lgsqrlem4  26734  lgsquadlem1  26765  2lgsoddprmlem2  26794  2sqlem3  26805  2sqlem8  26811  2sqblem  26816  2sqmod  26821  chebbnd1lem2  26855  chtppilimlem1  26858  chtppilim  26860  chto1ub  26861  vmadivsum  26867  rplogsumlem1  26869  rplogsumlem2  26870  dchrisum0lem1a  26871  rpvmasumlem  26872  dchrisumlem1  26874  dchrisumlem2  26875  dchrvmasumlem2  26883  dchrisum0flblem1  26893  dchrisum0flblem2  26894  dchrisum0lem1b  26900  dchrisum0lem1  26901  dchrisum0lem2a  26902  dchrisum0lem3  26904  dchrisum0  26905  mudivsum  26915  mulogsumlem  26916  mulog2sumlem1  26919  mulog2sumlem2  26920  2vmadivsumlem  26925  chpdifbndlem1  26938  selberg3lem1  26942  selberg4lem1  26945  pntrlog2bndlem1  26962  pntrlog2bndlem2  26963  pntrlog2bndlem3  26964  pntrlog2bndlem4  26965  pntpbnd1a  26970  pntpbnd1  26971  pntpbnd2  26972  pntibndlem2  26976  pntibndlem3  26977  pntlemd  26979  pntlemc  26980  pntlemb  26982  pntlemg  26983  pntlemh  26984  pntlemr  26987  pntlemf  26990  pntlemo  26992  abvcxp  27000  ostth2lem1  27003  padicabv  27015  ostth2lem2  27019  ostth2lem3  27020  ostth2lem4  27021  ostth2  27022  ostth3  27023  nodense  27077  nogt01o  27081  nosupbnd2lem1  27100  noetasuplem3  27120  maxs1  27150  maxs2  27151  cofcutr  27286  cofcutrtime  27289  addsunif  27353  negsunif  27393  tgcgr4  27536  legso  27604  krippenlem  27695  midex  27742  oppperpex  27758  ttgcontlem1  27896  axpaschlem  27952  axcontlem8  27983  upgrex  28106  nbfusgrlevtxm1  28388  finsumvtxdgeven  28563  wwlksnextproplem3  28919  clwlkclwwlk2  29010  clwlkclwwlkfolem  29014  clwwlkndivn  29087  ex-ind-dvds  29468  nvabs  29677  nmooge0  29772  nmoolb  29776  siii  29858  minvecolem2  29880  minvecolem4  29885  minvecolem5  29886  hlipgt0  29919  normge0  30131  normpyc  30151  pjhthlem1  30396  pjige0i  30695  nmoplb  30912  nmfnlb  30929  branmfn  31110  pjssdif2i  31179  stlei  31245  xlt2addrd  31731  eliccelico  31748  elicoelioo  31749  bcm1n  31766  dvdszzq  31781  prmdvdsbc  31782  fsumiunle  31795  pfxlsw2ccat  31876  wrdt2ind  31877  xrge0tsmsd  31969  omndmul2  31990  psgnfzto1stlem  32019  cycpmco2lem4  32048  cycpmco2lem5  32049  cyc3conja  32076  archirngz  32095  archiabllem2c  32101  ofldchr  32180  fedgmullem2  32412  extdggt0  32433  madjusmdetlem2  32498  locfinreflem  32510  xrge0iifiso  32605  nexple  32697  gsumesum  32747  esumcst  32751  esumpcvgval  32766  esumcvg  32774  esumiun  32782  measssd  32903  measunl  32904  omssubadd  32989  carsgclctunlem3  33009  pmeasmono  33013  sibfof  33029  oddpwdc  33043  eulerpartlemgc  33051  iwrdsplit  33076  ballotlemsgt1  33199  ballotlemsel1i  33201  sgnmul  33231  signsply0  33252  signstfvc  33275  signsvtp  33284  signsvfpn  33286  fdvposlt  33301  fdvneggt  33302  fdvnegge  33304  logdivsqrle  33352  hgt750lemf  33355  tgoldbachgtde  33362  swrdwlk  33807  subfaclim  33869  erdszelem7  33878  erdszelem8  33879  cvmliftlem2  33967  snmlff  34010  sinccvglem  34347  climlec3  34392  faclim  34405  fnejoin1  34916  poimirlem12  36163  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem23  36174  poimirlem28  36179  broucube  36185  mblfinlem2  36189  mblfinlem3  36190  mblfinlem4  36191  ismblfin  36192  itg2addnclem  36202  itg2addnclem3  36204  itg2gt0cn  36206  itggt0cn  36221  ftc1anclem5  36228  ftc1anclem7  36230  ftc1anclem8  36231  isbnd3  36316  ssbnd  36320  heiborlem8  36350  bfplem2  36355  rrncmslem  36364  rrnequiv  36367  rrntotbnd  36368  lcv1  37576  lsatcv0eq  37582  lsatcvat3  37587  cvlsupr2  37878  hlatlej2  37911  cvrval4N  37950  cvratlem  37957  atcvr0eq  37962  2atlt  37975  atbtwnex  37984  athgt  37992  1cvrat  38012  ps-1  38013  hlatexch3N  38016  hlatexch4  38017  3atlem2  38020  atcvrlln2  38055  lplnexllnN  38100  4atlem3a  38133  4atlem10b  38141  4atlem11b  38144  4atlem12b  38147  2lplnja  38155  dalemply  38190  dalemsly  38191  dalem1  38195  dalem6  38204  dalem7  38205  dalem-cly  38207  dalem11  38210  dalem12  38211  dalem16  38215  dalem17  38216  dalem38  38246  dalem44  38252  dalem61  38269  lnatexN  38315  lncvrat  38318  lncmp  38319  paddasslem2  38357  dalawlem3  38409  dalawlem6  38412  dalawlem11  38417  lhpmcvr  38559  lhp2atne  38570  lhp2at0ne  38572  lautj  38629  trlval4  38724  cdlemc2  38728  cdlemc5  38731  cdleme3b  38765  cdleme11c  38797  cdleme19a  38839  cdleme20j  38854  cdleme22f  38882  cdleme23c  38887  cdleme26f2ALTN  38900  cdleme26f2  38901  cdleme35fnpq  38985  cdleme48bw  39038  cdlemg10a  39176  cdlemg11b  39178  cdlemg17g  39203  cdlemg18c  39216  cdlemi1  39354  cdlemk52  39490  dia2dimlem1  39600  dihord1  39754  dihjatcclem4  39957  lcmineqlem15  40573  lcmineqlem19  40577  lcmineqlem22  40580  aks4d1lem1  40592  aks4d1p1p4  40601  aks4d1p1p5  40605  aks4d1p2  40607  aks4d1p3  40608  aks4d1p6  40611  aks4d1p7d1  40612  aks4d1p7  40613  aks4d1p8  40617  aks4d1p9  40618  sticksstones7  40633  metakunt7  40656  metakunt15  40664  metakunt16  40665  2xp3dxp2ge1d  40687  dvdsexpim  40872  dvdsexpnn0  40885  prjspner01  41021  flt4lem5  41046  fltnltalem  41058  fltnlta  41059  3cubeslem1  41065  eldioph2lem1  41141  lzenom  41151  irrapxlem1  41203  irrapxlem4  41206  irrapxlem5  41207  pell14qrgt0  41240  pell1qrge1  41251  pell1qrgap  41255  pellfundge  41263  pellfundex  41267  pellfund14  41279  rmspecsqrtnq  41287  rmxypos  41329  ltrmynn0  41330  ltrmxnn0  41331  jm2.24nn  41341  jm2.17b  41343  jm2.17c  41344  jm2.24  41345  congadd  41348  congsym  41350  congneg  41351  congid  41353  mzpcong  41354  acongrep  41362  acongeq  41365  jm2.18  41370  jm2.19  41375  jm2.23  41378  jm2.25  41381  jm2.26lem3  41383  jm2.15nn0  41385  jm2.16nn0  41386  jm2.27a  41387  jm2.27c  41389  jm3.1lem1  41399  idomrootle  41580  idomsubgmo  41583  sqrtcval  42035  inductionexd  42549  imo72b2  42567  dvgrat  42714  radcnvrat  42716  binomcxplemnn0  42751  binomcxplemnotnn0  42758  cncmpmax  43359  rnmptlb  43591  zltlesub  43640  infxrpnf  43801  xrpnf  43841  fmul01  43941  fmul01lt1lem1  43945  climdivf  43973  sumnnodd  43991  climinf2lem  44067  limsup10exlem  44133  climliminf  44167  dfxlim2v  44208  xlimliminflimsup  44223  dvdivbd  44284  volge0  44322  stoweidlem1  44362  stoweidlem16  44377  stoweidlem18  44379  stoweidlem24  44385  stoweidlem26  44387  stoweidlem36  44397  stoweidlem38  44399  stoweidlem41  44402  stoweidlem42  44403  stoweidlem44  44405  stoweidlem45  44406  stoweidlem48  44409  stoweidlem62  44423  wallispilem5  44430  stirlinglem1  44435  stirlinglem5  44439  stirlinglem7  44441  stirlinglem8  44442  stirlinglem9  44443  stirlinglem11  44445  fourierdlem4  44472  fourierdlem10  44478  fourierdlem37  44505  fourierdlem47  44514  fourierdlem72  44539  fourierdlem74  44541  fourierdlem79  44546  fourierdlem82  44549  fourierdlem89  44556  fourierdlem91  44558  fourierdlem93  44560  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  etransclem24  44619  etransclem25  44620  etransclem28  44623  etransclem37  44632  etransclem38  44633  etransclem44  44639  meaiuninc3v  44845  vonicclem1  45044  pimconstlt0  45062  smfsuplem1  45172  rlimdmafv  45529  rlimdmafv2  45610  2elfz2melfz  45670  iccpartgtprec  45732  iccpartlt  45736  iccpartgtl  45738  sqrtpwpw2p  45850  fmtnodvds  45856  goldbachthlem1  45857  lighneallem4a  45920  perfectALTVlem1  46033  cznnring  46374  rhmsubcrngc  46447  altgsumbcALT  46549  expnegico01  46719  flnn0div2ge  46739  rege1logbrege0  46764  fllogbd  46766  nnpw2blen  46786  nnolog2flm1  46796  dignn0ldlem  46808  dignn0flhalflem1  46821  dignn0flhalflem2  46822  eenglngeehlnmlem2  46944  itsclc0yqsol  46970  2itscp  46987  itscnhlinecirc02plem1  46988  itscnhlinecirc02plem2  46989  inlinecirc02p  46993