Theorem breqtrrd 5132

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  marypha1lem  9403  marypha2  9409  infsupprpr  9476  unxpwdom  9561  ttrcltr  9695  onadju  10243  nnadju  10247  cfss  10314  tskuni  10839  ltexnq  11031  lt2addmuld  12565  div4p1lem1div2  12570  nn0le2x  12629  mul2lt0rgt0  13194  prodge0ld  13199  ge2halflem1  13206  xrmax1  13274  xrmax2  13275  max1ALT  13285  qbtwnxr  13299  xleadd1a  13352  xlt2add  13359  xlesubadd  13362  xmulgt0  13382  xlemul1a  13387  xov1plusxeqvd  13598  uzsubsubfz  13648  fzctr  13742  subfzo0  13896  flflp1  13915  fldiv4lem1div2uz2  13944  ceilge  13953  modge0  13987  modlt  13988  modid  14004  m1modge3gt1  14029  modaddmodup  14045  sermono  14145  seqf1olem1  14152  seqf1olem2  14153  sqgt0  14237  sqge0  14247  leexp1a  14286  nnlesq  14316  expnbnd  14343  expmulnbnd  14346  discr1  14350  facwordi  14400  faclbnd5  14409  nfile  14470  hashdom  14490  hashgt23el  14536  fi1uzind  14619  brfi1indALT  14622  ccatdmss  14694  ccatws1n0  14747  swrds2  15058  sgnmul  15227  cjmulge0  15280  resqrtcl  15387  absge0  15421  sqreulem  15494  amgm2  15504  rlimdm  15685  rlimge0  15715  reccn2  15731  climle  15774  climserle  15797  isercoll2  15803  iseraltlem1  15816  iseralt  15819  isumclim2  15891  isumclim3  15892  isumge0  15899  fsumless  15930  cvgcmp  15950  cvgcmpce  15952  abscvgcvg  15953  isumsup2  15982  isumltss  15984  climcndslem1  15985  climcnds  15987  supcvg  15992  harmonic  15995  expcnv  16000  explecnv  16001  cvgrat  16019  mertenslem1  16020  mertenslem2  16021  clim2div  16025  ntrivcvgtail  16036  iprodclim2  16133  iprodclim3  16134  efcvg  16218  ege2le3  16223  efaddlem  16226  eftlub  16244  effsumlt  16246  tanhlt1  16295  ef01bndlem  16319  sin02gt0  16327  rpnnen2lem4  16352  ruclem2  16367  ruclem3  16368  ruclem9  16373  iddvdsexp  16416  dvdsadd  16439  dvdsfac  16463  dvdsexp2im  16464  dvdsmod  16466  3dvds  16468  omoe  16501  sumeven  16524  divalglem1  16531  flodddiv4t2lthalf  16555  bitsfzo  16572  bitsmod  16573  bitscmp  16575  bitsinv1lem  16578  sadcaddlem  16594  sadadd3  16598  sadaddlem  16603  dvdssqim  16691  dvdsexpim  16692  dvdsmulgcd  16693  nn0seqcvgd  16707  dvdslcm  16735  lcmgcdlem  16743  dvdslcmf  16768  lcmfunsnlem2lem2  16776  mulgcddvds  16792  qredeq  16794  cncongr2  16805  sqnprm  16840  isprm6  16852  dvdszzq  16859  prmdvdsbc  16864  nonsq  16897  hashdvds  16913  prmdiv  16923  odzdvds  16934  pythagtriplem4  16958  pcpre1  16981  pcdvdsb  17008  pcz  17020  pcprmpw2  17021  pcaddlem  17027  pcadd  17028  pcadd2  17029  pcmpt  17031  pcmptdvds  17033  fldivp1  17036  pcfaclem  17037  pockthlem  17044  prmreclem1  17055  prmreclem3  17057  prmreclem5  17059  prmreclem6  17060  4sqlem6  17082  4sqlem8  17084  4sqlem11  17094  4sqlem12  17095  4sqlem14  17097  4sqlem16  17099  vdwlem3  17122  vdwlem9  17128  vdwlem10  17129  vdwlem12  17131  ramub1lem2  17166  prmgap  17198  prmgaplcm  17199  prmgapprmo  17201  mreexexd  17783  invfuc  18113  ple1  18563  chnub  18757  eqgen  19354  lagsubg  19371  pgpfi  19780  sylow2alem2  19793  sylow2a  19794  sylow3lem4  19805  efgsrel  19909  odadd1  20023  odadd2  20024  gexex  20028  lt6abl  20070  dprd2d2  20221  dmdprdpr  20226  ablfacrp2  20244  ablfac1c  20248  pgpfaclem1  20258  ablfac2  20266  fincygsubgodd  20289  omndmul2  20308  dvdsrmul1  20560  unitmulclb  20572  subrguss  20800  rhmsubcrngc  20881  abvres  21049  znfld  21827  znunit  21830  ofldchr  21843  frlmisfrlm  22115  ply1coefsupp  22576  evl1gsumadd  22637  matgsum  22713  pm2mpcl  23076  psmetxrge0  24593  isxmet2d  24607  mettri  24632  xmettri3  24633  mettri3  24634  xmetrtri2  24636  prdsxmetlem  24648  imasdsf1olem  24653  xblss2ps  24681  blss2ps  24683  blss2  24684  blssps  24704  blss  24705  prdsbl  24771  dscmet  24852  nmge0  24897  nmmtri  24902  tngngp3  24936  nlmvscnlem2  24965  nrginvrcnlem  24971  nmoix  25009  nmoleub  25011  blcvx  25078  xrsxmet  25090  opnreen  25112  xrge0tsms  25115  icopnfcnv  25224  xrhmeo  25228  lebnumii  25248  pcophtb  25311  pi1grplem  25331  nmoleub2lem  25396  ipcau2  25516  tcphcphlem1  25517  ipcau  25520  ipcnlem2  25526  rrxcph  25674  minveclem2  25708  minveclem3b  25710  pjthlem1  25719  pjthlem2  25720  ivthlem3  25735  ivth2  25737  ovolfsf  25753  ovolsslem  25766  ovollb2lem  25770  ovollb2  25771  ovolctb  25772  ovolfiniun  25783  ovolicc1  25798  ovolicc2lem4  25802  ovolicc2  25804  nulmbl2  25818  unmbl  25819  ioombl1lem4  25843  uniioombllem4  25868  uniioombllem6  25870  volivth  25889  vitalilem4  25893  itg1ge0  25968  itg1ge0a  25993  itg1lea  25994  itg1climres  25996  mbfi1fseqlem5  26001  itg2ub  26015  itg2seq  26024  itg2uba  26025  itg2splitlem  26030  itg2split  26031  itg2monolem3  26034  itg2mono  26035  itg2i1fseq2  26038  itg2addlem  26040  iblss  26086  itggt0  26125  dvferm2lem  26267  dvlip  26274  dvivthlem1  26289  dvfsumlem2  26308  dvfsumlem3  26309  ftc1lem4  26320  ply1divmo  26415  ply1remlem  26444  fta1glem2  26448  idomrootle  26452  ig1pdvds  26459  plyeq0lem  26490  plydiveu  26582  fta1lem  26591  vieta1lem2  26597  aaliou3lem2  26633  aaliou3lem8  26635  ulmcn  26689  mtest  26694  itgulm  26698  radcnvlem1  26703  radcnvlt1  26708  dvradcnv  26711  pserdvlem2  26718  abelthlem2  26722  abelthlem6  26726  abelthlem7  26728  abelthlem9  26730  tangtx  26797  sinq12gt0  26799  sineq0  26815  cosordlem  26821  tanord  26829  tanregt0  26830  logrnaddcl  26865  logcj  26897  argregt0  26901  argrege0  26902  argimgt0  26903  argimlt0  26904  logimul  26905  logneg2  26906  logdivlti  26911  divlogrlim  26926  logcnlem3  26935  logcnlem4  26936  dvlog2lem  26943  logtayl  26951  rpcxpcl  26967  cxpsqrtlem  26993  cxpaddle  27043  isosctrlem1  27109  asinlem3a  27161  asinlem3  27162  asinneg  27177  asinsinlem  27182  asinsin  27183  atanlogaddlem  27204  atanlogadd  27205  atanlogsublem  27206  atanlogsub  27207  atantan  27214  atanbndlem  27216  atantayl  27228  leibpi  27233  birthdaylem3  27244  areaf  27252  cxploglim  27268  jensenlem2  27278  jensen  27279  logdiflbnd  27285  harmonicbnd4  27301  fsumharmonic  27302  zetacvg  27305  lgamgulmlem2  27320  lgamgulmlem3  27321  lgamcvg2  27345  wilthlem2  27359  wilthimp  27362  ftalem1  27363  ftalem2  27364  ftalem5  27367  basellem6  27376  basellem8  27378  basellem9  27379  chtge0  27402  chtublem  27501  logexprlim  27515  perfectlem1  27519  bcmax  27568  bposlem1  27574  bposlem2  27575  bposlem6  27579  bposlem7  27580  lgsdilem2  27623  lgsqrlem4  27639  lgsquadlem1  27670  2lgsoddprmlem2  27699  2sqlem3  27710  2sqlem8  27716  2sqblem  27721  2sqmod  27726  chebbnd1lem2  27760  chtppilimlem1  27763  chtppilim  27765  chto1ub  27766  vmadivsum  27772  rplogsumlem1  27774  rplogsumlem2  27775  dchrisum0lem1a  27776  rpvmasumlem  27777  dchrisumlem1  27779  dchrisumlem2  27780  dchrvmasumlem2  27788  dchrisum0flblem1  27798  dchrisum0flblem2  27799  dchrisum0lem1b  27805  dchrisum0lem1  27806  dchrisum0lem2a  27807  dchrisum0lem3  27809  dchrisum0  27810  mudivsum  27820  mulogsumlem  27821  mulog2sumlem1  27824  mulog2sumlem2  27825  2vmadivsumlem  27830  chpdifbndlem1  27843  selberg3lem1  27847  selberg4lem1  27850  pntrlog2bndlem1  27867  pntrlog2bndlem2  27868  pntrlog2bndlem3  27869  pntrlog2bndlem4  27870  pntpbnd1a  27875  pntpbnd1  27876  pntpbnd2  27877  pntibndlem2  27881  pntibndlem3  27882  pntlemd  27884  pntlemc  27885  pntlemb  27887  pntlemg  27888  pntlemh  27889  pntlemr  27892  pntlemf  27895  pntlemo  27897  abvcxp  27905  ostth2lem1  27908  padicabv  27920  ostth2lem2  27924  ostth2lem3  27925  ostth2lem4  27926  ostth2  27927  ostth3  27928  nodense  27982  nogt01o  27986  nosupbnd2lem1  28005  noetasuplem3  28025  maxs1  28059  maxs2  28060  eqcuts3  28123  cofcutr  28243  cofcutrtime  28246  addsuniflem  28320  negsunif  28374  sltmuls2  28467  precsexlem11  28536  abssge0  28564  leabss  28567  oncutlt  28583  om2noseqlt  28618  zsoring  28728  expsgt0  28756  halfcut  28777  addhalfcut  28778  bdayfinbndlem1  28786  elreno2  28814  tgcgr4  28927  legso  28995  krippenlem  29095  midex  29146  oppperpex  29162  angmgmaddcpbl  29323  angmgmaddlid  29325  angmgmaddrid  29326  prlngmid2  29372  prlngsymquadopp  29376  quadcgrprlng  29377  ttgcontlem1  29395  axpaschlem  29451  axcontlem8  29482  upgrex  29603  nbfusgrlevtxm1  29891  finsumvtxdgeven  30066  swrdwlk  30201  wwlksnextproplem3  30433  clwlkclwwlk2  30527  clwlkclwwlkfolem  30531  clwwlkndivn  30604  ex-ind-dvds  30995  nvabs  31207  nmooge0  31302  nmoolb  31306  siii  31388  minvecolem2  31410  minvecolem4  31415  minvecolem5  31416  hlipgt0  31449  normge0  31661  normpyc  31681  pjhthlem1  31926  pjige0i  32225  nmoplb  32442  nmfnlb  32459  branmfn  32640  pjssdif2i  32709  stlei  32775  xlt2addrd  33284  eliccelico  33302  elicoelioo  33303  bcm1n  33320  fsumiunle  33353  nexple  33357  expevenpos  33359  pfxlsw2ccat  33446  wrdt2ind  33449  xrge0tsmsd  33567  gsumwrd2dccatlem  33571  psgnfzto1stlem  33594  cycpmco2lem4  33623  cycpmco2lem5  33624  cyc3conja  33651  archirngz  33683  archiabllem2c  33689  rprmasso2  33991  rprmirred  33996  1arithufdlem3  34011  vietadeg1  34143  lbslelsp  34163  fedgmullem2  34195  extdggt0  34222  evls1fldgencl  34235  fldextrspunlem1  34240  extdgfialglem1  34257  algextdeglem8  34289  rtelextdg2lem  34291  cos9thpiminplylem1  34347  cos9thpiminplylem2  34348  madjusmdetlem2  34393  locfinreflem  34405  xrge0iifiso  34500  gsumesum  34624  esumcst  34628  esumpcvgval  34643  esumcvg  34651  esumiun  34659  measssd  34781  measunl  34782  omssubadd  34866  carsgclctunlem3  34886  pmeasmono  34890  sibfof  34906  oddpwdc  34920  eulerpartlemgc  34928  iwrdsplit  34953  ballotlemsgt1  35077  ballotlemsel1i  35079  signsply0  35114  signstfvc  35137  signsvtp  35146  signsvfpn  35148  fdvposlt  35162  fdvneggt  35163  fdvnegge  35165  logdivsqrle  35213  hgt750lemf  35216  tgoldbachgtde  35223  subfaclim  35874  erdszelem7  35883  erdszelem8  35884  cvmliftlem2  35972  snmlff  36015  sinccvglem  36358  climlec3  36420  faclim  36432  fnejoin1  37078  poimirlem12  38470  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  poimirlem23  38481  poimirlem28  38486  broucube  38492  mblfinlem2  38496  mblfinlem3  38497  mblfinlem4  38498  ismblfin  38499  itg2addnclem  38509  itg2addnclem3  38511  itg2gt0cn  38513  itggt0cn  38528  ftc1anclem5  38535  ftc1anclem7  38537  ftc1anclem8  38538  isbnd3  38638  ssbnd  38642  heiborlem8  38672  bfplem2  38677  rrncmslem  38686  rrnequiv  38689  rrntotbnd  38690  lcv1  40018  lsatcv0eq  40024  lsatcvat3  40029  cvlsupr2  40320  hlatlej2  40353  cvrval4N  40391  cvratlem  40398  atcvr0eq  40403  2atlt  40416  atbtwnex  40425  athgt  40433  1cvrat  40453  ps-1  40454  hlatexch3N  40457  hlatexch4  40458  3atlem2  40461  atcvrlln2  40496  lplnexllnN  40541  4atlem3a  40574  4atlem10b  40582  4atlem11b  40585  4atlem12b  40588  2lplnja  40596  dalemply  40631  dalemsly  40632  dalem1  40636  dalem6  40645  dalem7  40646  dalem-cly  40648  dalem11  40651  dalem12  40652  dalem16  40656  dalem17  40657  dalem38  40687  dalem44  40693  dalem61  40710  lnatexN  40756  lncvrat  40759  lncmp  40760  paddasslem2  40798  dalawlem3  40850  dalawlem6  40853  dalawlem11  40858  lhpmcvr  41000  lhp2atne  41011  lhp2at0ne  41013  lautj  41070  trlval4  41165  cdlemc2  41169  cdlemc5  41172  cdleme3b  41206  cdleme11c  41238  cdleme19a  41280  cdleme20j  41295  cdleme22f  41323  cdleme23c  41328  cdleme26f2ALTN  41341  cdleme26f2  41342  cdleme35fnpq  41426  cdleme48bw  41479  cdlemg10a  41617  cdlemg11b  41619  cdlemg17g  41644  cdlemg18c  41657  cdlemi1  41795  cdlemk52  41931  dia2dimlem1  42041  dihord1  42195  dihjatcclem4  42398  lcmineqlem15  43013  lcmineqlem19  43017  lcmineqlem22  43020  aks4d1lem1  43032  aks4d1p1p4  43041  aks4d1p1p5  43045  aks4d1p2  43047  aks4d1p3  43048  aks4d1p6  43051  aks4d1p7d1  43052  aks4d1p7  43053  aks4d1p8  43057  aks4d1p9  43058  aks6d1c1p6  43084  aks6d1c1  43086  aks6d1c2  43100  sticksstones7  43122  aks6d1c7lem1  43150  unitscyglem4  43168  dvdsexpnn0  43313  prjspner01  43575  flt4lem5  43600  fltnltalem  43612  fltnlta  43613  3cubeslem1  43633  eldioph2lem1  43709  lzenom  43719  irrapxlem1  43767  irrapxlem4  43770  irrapxlem5  43771  pell14qrgt0  43804  pell1qrge1  43815  pell1qrgap  43819  pellfundge  43827  pellfundex  43831  pellfund14  43843  rmspecsqrtnq  43851  rmxypos  43892  ltrmynn0  43893  ltrmxnn0  43894  jm2.24nn  43904  jm2.17b  43906  jm2.17c  43907  jm2.24  43908  congadd  43911  congsym  43913  congneg  43914  congid  43916  mzpcong  43917  acongrep  43925  acongeq  43928  jm2.18  43933  jm2.19  43938  jm2.23  43941  jm2.25  43944  jm2.26lem3  43946  jm2.15nn0  43948  jm2.16nn0  43949  jm2.27a  43950  jm2.27c  43952  jm3.1lem1  43962  idomsubgmo  44138  sqrtcval  44585  inductionexd  45099  imo72b2lem0  45109  imo72b2  45116  dvgrat  45240  radcnvrat  45242  binomcxplemnn0  45277  binomcxplemnotnn0  45284  cncmpmax  45970  rnmptlb  46176  zltlesub  46222  infxrpnf  46378  xrpnf  46417  fmul01  46514  fmul01lt1lem1  46518  climdivf  46546  sumnnodd  46564  climinf2lem  46638  limsup10exlem  46704  climliminf  46738  dfxlim2v  46779  xlimliminflimsup  46794  dvdivbd  46855  volge0  46893  stoweidlem1  46933  stoweidlem16  46948  stoweidlem18  46950  stoweidlem24  46956  stoweidlem26  46958  stoweidlem36  46968  stoweidlem38  46970  stoweidlem41  46973  stoweidlem42  46974  stoweidlem44  46976  stoweidlem45  46977  stoweidlem48  46980  stoweidlem62  46994  wallispilem5  47001  stirlinglem1  47006  stirlinglem5  47010  stirlinglem7  47012  stirlinglem8  47013  stirlinglem9  47014  stirlinglem11  47016  fourierdlem4  47043  fourierdlem10  47049  fourierdlem37  47076  fourierdlem47  47085  fourierdlem72  47110  fourierdlem74  47112  fourierdlem79  47117  fourierdlem82  47120  fourierdlem89  47127  fourierdlem91  47129  fourierdlem93  47131  fourierdlem103  47141  fourierdlem104  47142  fourierdlem112  47150  etransclem24  47190  etransclem25  47191  etransclem28  47194  etransclem37  47203  etransclem38  47204  etransclem44  47210  meaiuninc3v  47416  vonicclem1  47615  pimconstlt0  47633  smfsuplem1  47743  chnerlem1  47814  rlimdmafv  48169  rlimdmafv2  48250  2elfz2melfz  48310  2timesltsq  48370  muldvdsfacgt  48378  iccpartgtprec  48424  iccpartlt  48428  iccpartgtl  48430  sqrtpwpw2p  48545  fmtnodvds  48551  goldbachthlem1  48552  lighneallem4a  48615  nprmdvdsfacm1lem1  48627  perfectALTVlem1  48741  uhgrimgrlim  49007  cznnring  49281  altgsumbcALT  49387  expnegico01  49552  flnn0div2ge  49567  rege1logbrege0  49592  fllogbd  49594  nnpw2blen  49614  nnolog2flm1  49624  dignn0ldlem  49636  dignn0flhalflem1  49649  dignn0flhalflem2  49650  eenglngeehlnmlem2  49772  itsclc0yqsol  49798  2itscp  49815  itscnhlinecirc02plem1  49816  itscnhlinecirc02plem2  49817  inlinecirc02p  49821