Theorem breqtrrd 5130

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

Syntax hints:   → wi 4   = wceq 1562   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 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  marypha1lem  9381  marypha2  9387  infsupprpr  9454  unxpwdom  9539  ttrcltr  9673  onadju  10152  nnadju  10156  cfss  10224  tskuni  10743  ltexnq  10935  lt2addmuld  12473  div4p1lem1div2  12478  nn0le2x  12537  mul2lt0rgt0  13100  prodge0ld  13105  ge2halflem1  13112  xrmax1  13180  xrmax2  13181  max1ALT  13191  qbtwnxr  13205  xleadd1a  13258  xlt2add  13265  xlesubadd  13268  xmulgt0  13288  xlemul1a  13293  xov1plusxeqvd  13504  uzsubsubfz  13553  fzctr  13647  subfzo0  13800  flflp1  13819  fldiv4lem1div2uz2  13848  ceilge  13857  modge0  13891  modlt  13892  modid  13908  m1modge3gt1  13933  modaddmodup  13949  sermono  14049  seqf1olem1  14056  seqf1olem2  14057  sqgt0  14141  sqge0  14151  leexp1a  14190  nnlesq  14220  expnbnd  14247  expmulnbnd  14250  discr1  14254  facwordi  14304  faclbnd5  14313  nfile  14374  hashdom  14394  hashgt23el  14439  fi1uzind  14522  brfi1indALT  14525  ccatdmss  14597  ccatws1n0  14648  swrds2  14955  sgnmul  15122  cjmulge0  15175  resqrtcl  15282  absge0  15316  sqreulem  15389  amgm2  15399  rlimdm  15580  rlimge0  15610  reccn2  15626  climle  15669  climserle  15692  isercoll2  15698  iseraltlem1  15711  iseralt  15714  isumclim2  15787  isumclim3  15788  isumge0  15795  fsumless  15826  cvgcmp  15846  cvgcmpce  15848  abscvgcvg  15849  isumsup2  15878  isumltss  15880  climcndslem1  15881  climcnds  15883  supcvg  15888  harmonic  15891  expcnv  15896  explecnv  15897  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  clim2div  15921  ntrivcvgtail  15932  iprodclim2  16031  iprodclim3  16032  efcvg  16117  ege2le3  16122  efaddlem  16125  eftlub  16143  effsumlt  16145  tanhlt1  16194  ef01bndlem  16218  sin02gt0  16226  rpnnen2lem4  16251  ruclem2  16266  ruclem3  16267  ruclem9  16272  iddvdsexp  16315  dvdsadd  16338  dvdsfac  16362  dvdsexp2im  16363  dvdsmod  16365  3dvds  16367  omoe  16400  sumeven  16423  divalglem1  16430  flodddiv4t2lthalf  16454  bitsfzo  16471  bitsmod  16472  bitscmp  16474  bitsinv1lem  16477  sadcaddlem  16493  sadadd3  16497  sadaddlem  16502  dvdssqim  16590  dvdsexpim  16591  dvdsmulgcd  16592  nn0seqcvgd  16606  dvdslcm  16634  lcmgcdlem  16642  dvdslcmf  16667  lcmfunsnlem2lem2  16675  mulgcddvds  16691  qredeq  16693  cncongr2  16704  sqnprm  16739  isprm6  16751  dvdszzq  16758  prmdvdsbc  16763  nonsq  16796  hashdvds  16812  prmdiv  16822  odzdvds  16833  pythagtriplem4  16857  pcpre1  16880  pcdvdsb  16907  pcz  16919  pcprmpw2  16920  pcaddlem  16926  pcadd  16927  pcadd2  16928  pcmpt  16930  pcmptdvds  16932  fldivp1  16935  pcfaclem  16936  pockthlem  16943  prmreclem1  16954  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  4sqlem6  16981  4sqlem8  16983  4sqlem11  16993  4sqlem12  16994  4sqlem14  16996  4sqlem16  16998  vdwlem3  17021  vdwlem9  17027  vdwlem10  17028  vdwlem12  17030  ramub1lem2  17065  prmgap  17097  prmgaplcm  17098  prmgapprmo  17100  mreexexd  17682  invfuc  18012  ple1  18462  chnub  18656  eqgen  19224  lagsubg  19238  pgpfi  19647  sylow2alem2  19660  sylow2a  19661  sylow3lem4  19672  efgsrel  19776  odadd1  19890  odadd2  19891  gexex  19895  lt6abl  19937  dprd2d2  20088  dmdprdpr  20093  ablfacrp2  20111  ablfac1c  20115  pgpfaclem1  20125  ablfac2  20133  fincygsubgodd  20156  omndmul2  20175  dvdsrmul1  20420  unitmulclb  20432  subrguss  20639  rhmsubcrngc  20720  abvres  20882  znfld  21614  znunit  21617  ofldchr  21630  frlmisfrlm  21902  ply1coefsupp  22362  evl1gsumadd  22423  matgsum  22499  pm2mpcl  22859  psmetxrge0  24375  isxmet2d  24389  mettri  24414  xmettri3  24415  mettri3  24416  xmetrtri2  24418  prdsxmetlem  24430  imasdsf1olem  24435  xblss2ps  24463  blss2ps  24465  blss2  24466  blssps  24486  blss  24487  prdsbl  24553  dscmet  24634  nmge0  24679  nmmtri  24684  tngngp3  24718  nlmvscnlem2  24747  nrginvrcnlem  24753  nmoix  24791  nmoleub  24793  blcvx  24860  xrsxmet  24872  opnreen  24894  xrge0tsms  24897  icopnfcnv  25006  xrhmeo  25010  lebnumii  25030  pcophtb  25093  pi1grplem  25113  nmoleub2lem  25178  ipcau2  25298  tcphcphlem1  25299  ipcau  25302  ipcnlem2  25308  rrxcph  25456  minveclem2  25490  minveclem3b  25492  pjthlem1  25501  pjthlem2  25502  ivthlem3  25517  ivth2  25519  ovolfsf  25535  ovolsslem  25548  ovollb2lem  25552  ovollb2  25553  ovolctb  25554  ovolfiniun  25565  ovolicc1  25580  ovolicc2lem4  25584  ovolicc2  25586  nulmbl2  25600  unmbl  25601  ioombl1lem4  25625  uniioombllem4  25650  uniioombllem6  25652  volivth  25671  vitalilem4  25675  itg1ge0  25750  itg1ge0a  25775  itg1lea  25776  itg1climres  25778  mbfi1fseqlem5  25783  itg2ub  25797  itg2seq  25806  itg2uba  25807  itg2splitlem  25812  itg2split  25813  itg2monolem3  25816  itg2mono  25817  itg2i1fseq2  25820  itg2addlem  25822  iblss  25869  itggt0  25908  dvferm2lem  26050  dvlip  26057  dvivthlem1  26072  dvfsumlem2  26091  dvfsumlem3  26092  ftc1lem4  26103  ply1divmo  26198  ply1remlem  26227  fta1glem2  26231  idomrootle  26235  ig1pdvds  26242  plyeq0lem  26272  plydiveu  26364  fta1lem  26373  vieta1lem2  26377  aaliou3lem2  26409  aaliou3lem8  26411  ulmcn  26464  mtest  26469  itgulm  26473  radcnvlem1  26478  radcnvlt1  26483  dvradcnv  26486  pserdvlem2  26493  abelthlem2  26497  abelthlem6  26501  abelthlem7  26503  abelthlem9  26505  tangtx  26572  sinq12gt0  26574  sineq0  26591  cosordlem  26597  tanord  26605  tanregt0  26606  logrnaddcl  26641  logcj  26673  argregt0  26677  argrege0  26678  argimgt0  26679  argimlt0  26680  logimul  26681  logneg2  26682  logdivlti  26687  divlogrlim  26702  logcnlem3  26711  logcnlem4  26712  dvlog2lem  26719  logtayl  26727  rpcxpcl  26743  cxpsqrtlem  26769  cxpaddle  26819  isosctrlem1  26885  asinlem3a  26937  asinlem3  26938  asinneg  26953  asinsinlem  26958  asinsin  26959  atanlogaddlem  26980  atanlogadd  26981  atanlogsublem  26982  atanlogsub  26983  atantan  26990  atanbndlem  26992  atantayl  27004  leibpi  27009  birthdaylem3  27020  areaf  27028  cxploglim  27044  jensenlem2  27054  jensen  27055  logdiflbnd  27061  harmonicbnd4  27077  fsumharmonic  27078  zetacvg  27081  lgamgulmlem2  27096  lgamgulmlem3  27097  lgamcvg2  27121  wilthlem2  27135  wilthimp  27138  ftalem1  27139  ftalem2  27140  ftalem5  27143  basellem6  27152  basellem8  27154  basellem9  27155  chtge0  27178  chtublem  27277  logexprlim  27291  perfectlem1  27295  bcmax  27344  bposlem1  27350  bposlem2  27351  bposlem6  27355  bposlem7  27356  lgsdilem2  27399  lgsqrlem4  27415  lgsquadlem1  27446  2lgsoddprmlem2  27475  2sqlem3  27486  2sqlem8  27492  2sqblem  27497  2sqmod  27502  chebbnd1lem2  27536  chtppilimlem1  27539  chtppilim  27541  chto1ub  27542  vmadivsum  27548  rplogsumlem1  27550  rplogsumlem2  27551  dchrisum0lem1a  27552  rpvmasumlem  27553  dchrisumlem1  27555  dchrisumlem2  27556  dchrvmasumlem2  27564  dchrisum0flblem1  27574  dchrisum0flblem2  27575  dchrisum0lem1b  27581  dchrisum0lem1  27582  dchrisum0lem2a  27583  dchrisum0lem3  27585  dchrisum0  27586  mudivsum  27596  mulogsumlem  27597  mulog2sumlem1  27600  mulog2sumlem2  27601  2vmadivsumlem  27606  chpdifbndlem1  27619  selberg3lem1  27623  selberg4lem1  27626  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntpbnd1a  27651  pntpbnd1  27652  pntpbnd2  27653  pntibndlem2  27657  pntibndlem3  27658  pntlemd  27660  pntlemc  27661  pntlemb  27663  pntlemg  27664  pntlemh  27665  pntlemr  27668  pntlemf  27671  pntlemo  27673  abvcxp  27681  ostth2lem1  27684  padicabv  27696  ostth2lem2  27700  ostth2lem3  27701  ostth2lem4  27702  ostth2  27703  ostth3  27704  nodense  27758  nogt01o  27762  nosupbnd2lem1  27781  noetasuplem3  27801  maxs1  27835  maxs2  27836  eqcuts3  27899  cofcutr  28019  cofcutrtime  28022  addsuniflem  28096  negsunif  28150  sltmuls2  28243  precsexlem11  28312  abssge0  28340  leabss  28343  oncutlt  28359  om2noseqlt  28394  zsoring  28504  expsgt0  28532  halfcut  28553  addhalfcut  28554  bdayfinbndlem1  28562  elreno2  28590  tgcgr4  28702  legso  28770  krippenlem  28865  midex  28912  oppperpex  28928  ttgcontlem1  29087  axpaschlem  29143  axcontlem8  29174  upgrex  29295  nbfusgrlevtxm1  29580  finsumvtxdgeven  29755  wwlksnextproplem3  30113  clwlkclwwlk2  30207  clwlkclwwlkfolem  30211  clwwlkndivn  30284  ex-ind-dvds  30665  nvabs  30877  nmooge0  30972  nmoolb  30976  siii  31058  minvecolem2  31080  minvecolem4  31085  minvecolem5  31086  hlipgt0  31119  normge0  31331  normpyc  31351  pjhthlem1  31596  pjige0i  31895  nmoplb  32112  nmfnlb  32129  branmfn  32310  pjssdif2i  32379  stlei  32445  xlt2addrd  32963  eliccelico  32981  elicoelioo  32982  bcm1n  32999  fsumiunle  33033  nexple  33037  expevenpos  33039  pfxlsw2ccat  33130  wrdt2ind  33133  xrge0tsmsd  33255  gsumwrd2dccatlem  33259  psgnfzto1stlem  33282  cycpmco2lem4  33311  cycpmco2lem5  33312  cyc3conja  33339  archirngz  33371  archiabllem2c  33377  rprmasso2  33724  rprmirred  33729  1arithufdlem3  33744  vietadeg1  33877  lbslelsp  33897  fedgmullem2  33929  extdggt0  33956  evls1fldgencl  33969  fldextrspunlem1  33974  extdgfialglem1  33991  algextdeglem8  34023  rtelextdg2lem  34025  cos9thpiminplylem1  34081  cos9thpiminplylem2  34082  madjusmdetlem2  34127  locfinreflem  34139  xrge0iifiso  34234  gsumesum  34358  esumcst  34362  esumpcvgval  34377  esumcvg  34385  esumiun  34393  measssd  34514  measunl  34515  omssubadd  34599  carsgclctunlem3  34619  pmeasmono  34623  sibfof  34639  oddpwdc  34653  eulerpartlemgc  34661  iwrdsplit  34686  ballotlemsgt1  34810  ballotlemsel1i  34812  signsply0  34847  signstfvc  34870  signsvtp  34879  signsvfpn  34881  fdvposlt  34895  fdvneggt  34896  fdvnegge  34898  logdivsqrle  34946  hgt750lemf  34949  tgoldbachgtde  34956  swrdwlk  35482  subfaclim  35543  erdszelem7  35552  erdszelem8  35553  cvmliftlem2  35641  snmlff  35684  sinccvglem  36027  climlec3  36089  faclim  36101  fnejoin1  36733  poimirlem12  38136  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem23  38147  poimirlem28  38152  broucube  38158  mblfinlem2  38162  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  itg2addnclem  38175  itg2addnclem3  38177  itg2gt0cn  38179  itggt0cn  38194  ftc1anclem5  38201  ftc1anclem7  38203  ftc1anclem8  38204  isbnd3  38288  ssbnd  38292  heiborlem8  38322  bfplem2  38327  rrncmslem  38336  rrnequiv  38339  rrntotbnd  38340  lcv1  39670  lsatcv0eq  39676  lsatcvat3  39681  cvlsupr2  39972  hlatlej2  40005  cvrval4N  40043  cvratlem  40050  atcvr0eq  40055  2atlt  40068  atbtwnex  40077  athgt  40085  1cvrat  40105  ps-1  40106  hlatexch3N  40109  hlatexch4  40110  3atlem2  40113  atcvrlln2  40148  lplnexllnN  40193  4atlem3a  40226  4atlem10b  40234  4atlem11b  40237  4atlem12b  40240  2lplnja  40248  dalemply  40283  dalemsly  40284  dalem1  40288  dalem6  40297  dalem7  40298  dalem-cly  40300  dalem11  40303  dalem12  40304  dalem16  40308  dalem17  40309  dalem38  40339  dalem44  40345  dalem61  40362  lnatexN  40408  lncvrat  40411  lncmp  40412  paddasslem2  40450  dalawlem3  40502  dalawlem6  40505  dalawlem11  40510  lhpmcvr  40652  lhp2atne  40663  lhp2at0ne  40665  lautj  40722  trlval4  40817  cdlemc2  40821  cdlemc5  40824  cdleme3b  40858  cdleme11c  40890  cdleme19a  40932  cdleme20j  40947  cdleme22f  40975  cdleme23c  40980  cdleme26f2ALTN  40993  cdleme26f2  40994  cdleme35fnpq  41078  cdleme48bw  41131  cdlemg10a  41269  cdlemg11b  41271  cdlemg17g  41296  cdlemg18c  41309  cdlemi1  41447  cdlemk52  41583  dia2dimlem1  41693  dihord1  41847  dihjatcclem4  42050  lcmineqlem15  42665  lcmineqlem19  42669  lcmineqlem22  42672  aks4d1lem1  42684  aks4d1p1p4  42693  aks4d1p1p5  42697  aks4d1p2  42699  aks4d1p3  42700  aks4d1p6  42703  aks4d1p7d1  42704  aks4d1p7  42705  aks4d1p8  42709  aks4d1p9  42710  aks6d1c1p6  42736  aks6d1c1  42738  aks6d1c2  42752  sticksstones7  42774  aks6d1c7lem1  42802  unitscyglem4  42820  dvdsexpnn0  42948  prjspner01  43212  flt4lem5  43237  fltnltalem  43249  fltnlta  43250  3cubeslem1  43270  eldioph2lem1  43346  lzenom  43356  irrapxlem1  43404  irrapxlem4  43407  irrapxlem5  43408  pell14qrgt0  43441  pell1qrge1  43452  pell1qrgap  43456  pellfundge  43464  pellfundex  43468  pellfund14  43480  rmspecsqrtnq  43488  rmxypos  43529  ltrmynn0  43530  ltrmxnn0  43531  jm2.24nn  43541  jm2.17b  43543  jm2.17c  43544  jm2.24  43545  congadd  43548  congsym  43550  congneg  43551  congid  43553  mzpcong  43554  acongrep  43562  acongeq  43565  jm2.18  43570  jm2.19  43575  jm2.23  43578  jm2.25  43581  jm2.26lem3  43583  jm2.15nn0  43585  jm2.16nn0  43586  jm2.27a  43587  jm2.27c  43589  jm3.1lem1  43599  idomsubgmo  43775  sqrtcval  44222  inductionexd  44736  imo72b2lem0  44746  imo72b2  44753  dvgrat  44893  radcnvrat  44895  binomcxplemnn0  44930  binomcxplemnotnn0  44937  cncmpmax  45617  rnmptlb  45823  zltlesub  45869  infxrpnf  46025  xrpnf  46064  fmul01  46161  fmul01lt1lem1  46165  climdivf  46193  sumnnodd  46211  climinf2lem  46285  limsup10exlem  46351  climliminf  46385  dfxlim2v  46426  xlimliminflimsup  46441  dvdivbd  46502  volge0  46540  stoweidlem1  46580  stoweidlem16  46595  stoweidlem18  46597  stoweidlem24  46603  stoweidlem26  46605  stoweidlem36  46615  stoweidlem38  46617  stoweidlem41  46620  stoweidlem42  46621  stoweidlem44  46623  stoweidlem45  46624  stoweidlem48  46627  stoweidlem62  46641  wallispilem5  46648  stirlinglem1  46653  stirlinglem5  46657  stirlinglem7  46659  stirlinglem8  46660  stirlinglem9  46661  stirlinglem11  46663  fourierdlem4  46690  fourierdlem10  46696  fourierdlem37  46723  fourierdlem47  46732  fourierdlem72  46757  fourierdlem74  46759  fourierdlem79  46764  fourierdlem82  46767  fourierdlem89  46774  fourierdlem91  46776  fourierdlem93  46778  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  etransclem24  46837  etransclem25  46838  etransclem28  46841  etransclem37  46850  etransclem38  46851  etransclem44  46857  meaiuninc3v  47063  vonicclem1  47262  pimconstlt0  47280  smfsuplem1  47390  chnerlem1  47463  rlimdmafv  47776  rlimdmafv2  47857  2elfz2melfz  47917  2timesltsq  47977  muldvdsfacgt  47985  iccpartgtprec  48031  iccpartlt  48035  iccpartgtl  48037  sqrtpwpw2p  48152  fmtnodvds  48158  goldbachthlem1  48159  lighneallem4a  48222  nprmdvdsfacm1lem1  48234  perfectALTVlem1  48348  uhgrimgrlim  48614  cznnring  48889  altgsumbcALT  48980  expnegico01  49145  flnn0div2ge  49160  rege1logbrege0  49185  fllogbd  49187  nnpw2blen  49207  nnolog2flm1  49217  dignn0ldlem  49229  dignn0flhalflem1  49242  dignn0flhalflem2  49243  eenglngeehlnmlem2  49365  itsclc0yqsol  49391  2itscp  49408  itscnhlinecirc02plem1  49409  itscnhlinecirc02plem2  49410  inlinecirc02p  49414