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

Syntax hints:   → wi 4   = wceq 1568   class class class wbr 5108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is referenced by:  marypha1lem  9392  marypha2  9398  infsupprpr  9465  unxpwdom  9550  ttrcltr  9684  onadju  10176  nnadju  10180  cfss  10248  tskuni  10767  ltexnq  10959  lt2addmuld  12493  div4p1lem1div2  12498  nn0le2x  12557  mul2lt0rgt0  13120  prodge0ld  13125  ge2halflem1  13132  xrmax1  13200  xrmax2  13201  max1ALT  13211  qbtwnxr  13225  xleadd1a  13278  xlt2add  13285  xlesubadd  13288  xmulgt0  13308  xlemul1a  13313  xov1plusxeqvd  13524  uzsubsubfz  13573  fzctr  13667  subfzo0  13820  flflp1  13839  fldiv4lem1div2uz2  13868  ceilge  13877  modge0  13911  modlt  13912  modid  13928  m1modge3gt1  13953  modaddmodup  13969  sermono  14069  seqf1olem1  14076  seqf1olem2  14077  sqgt0  14161  sqge0  14171  leexp1a  14210  nnlesq  14240  expnbnd  14267  expmulnbnd  14270  discr1  14274  facwordi  14324  faclbnd5  14333  nfile  14394  hashdom  14414  hashgt23el  14460  fi1uzind  14543  brfi1indALT  14546  ccatdmss  14618  ccatws1n0  14669  swrds2  14976  sgnmul  15143  cjmulge0  15196  resqrtcl  15303  absge0  15337  sqreulem  15410  amgm2  15420  rlimdm  15601  rlimge0  15631  reccn2  15647  climle  15690  climserle  15713  isercoll2  15719  iseraltlem1  15732  iseralt  15735  isumclim2  15808  isumclim3  15809  isumge0  15816  fsumless  15847  cvgcmp  15867  cvgcmpce  15869  abscvgcvg  15870  isumsup2  15899  isumltss  15901  climcndslem1  15902  climcnds  15904  supcvg  15909  harmonic  15912  expcnv  15917  explecnv  15918  cvgrat  15936  mertenslem1  15937  mertenslem2  15938  clim2div  15942  ntrivcvgtail  15953  iprodclim2  16052  iprodclim3  16053  efcvg  16138  ege2le3  16143  efaddlem  16146  eftlub  16164  effsumlt  16166  tanhlt1  16215  ef01bndlem  16239  sin02gt0  16247  rpnnen2lem4  16272  ruclem2  16287  ruclem3  16288  ruclem9  16293  iddvdsexp  16336  dvdsadd  16359  dvdsfac  16383  dvdsexp2im  16384  dvdsmod  16386  3dvds  16388  omoe  16421  sumeven  16444  divalglem1  16451  flodddiv4t2lthalf  16475  bitsfzo  16492  bitsmod  16493  bitscmp  16495  bitsinv1lem  16498  sadcaddlem  16514  sadadd3  16518  sadaddlem  16523  dvdssqim  16611  dvdsexpim  16612  dvdsmulgcd  16613  nn0seqcvgd  16627  dvdslcm  16655  lcmgcdlem  16663  dvdslcmf  16688  lcmfunsnlem2lem2  16696  mulgcddvds  16712  qredeq  16714  cncongr2  16725  sqnprm  16760  isprm6  16772  dvdszzq  16779  prmdvdsbc  16784  nonsq  16817  hashdvds  16833  prmdiv  16843  odzdvds  16854  pythagtriplem4  16878  pcpre1  16901  pcdvdsb  16928  pcz  16940  pcprmpw2  16941  pcaddlem  16947  pcadd  16948  pcadd2  16949  pcmpt  16951  pcmptdvds  16953  fldivp1  16956  pcfaclem  16957  pockthlem  16964  prmreclem1  16975  prmreclem3  16977  prmreclem5  16979  prmreclem6  16980  4sqlem6  17002  4sqlem8  17004  4sqlem11  17014  4sqlem12  17015  4sqlem14  17017  4sqlem16  17019  vdwlem3  17042  vdwlem9  17048  vdwlem10  17049  vdwlem12  17051  ramub1lem2  17086  prmgap  17118  prmgaplcm  17119  prmgapprmo  17121  mreexexd  17703  invfuc  18033  ple1  18483  chnub  18677  eqgen  19248  lagsubg  19265  pgpfi  19674  sylow2alem2  19687  sylow2a  19688  sylow3lem4  19699  efgsrel  19803  odadd1  19917  odadd2  19918  gexex  19922  lt6abl  19964  dprd2d2  20115  dmdprdpr  20120  ablfacrp2  20138  ablfac1c  20142  pgpfaclem1  20152  ablfac2  20160  fincygsubgodd  20183  omndmul2  20202  dvdsrmul1  20450  unitmulclb  20462  subrguss  20671  rhmsubcrngc  20752  abvres  20913  znfld  21689  znunit  21692  ofldchr  21705  frlmisfrlm  21977  ply1coefsupp  22436  evl1gsumadd  22497  matgsum  22573  pm2mpcl  22933  psmetxrge0  24449  isxmet2d  24463  mettri  24488  xmettri3  24489  mettri3  24490  xmetrtri2  24492  prdsxmetlem  24504  imasdsf1olem  24509  xblss2ps  24537  blss2ps  24539  blss2  24540  blssps  24560  blss  24561  prdsbl  24627  dscmet  24708  nmge0  24753  nmmtri  24758  tngngp3  24792  nlmvscnlem2  24821  nrginvrcnlem  24827  nmoix  24865  nmoleub  24867  blcvx  24934  xrsxmet  24946  opnreen  24968  xrge0tsms  24971  icopnfcnv  25080  xrhmeo  25084  lebnumii  25104  pcophtb  25167  pi1grplem  25187  nmoleub2lem  25252  ipcau2  25372  tcphcphlem1  25373  ipcau  25376  ipcnlem2  25382  rrxcph  25530  minveclem2  25564  minveclem3b  25566  pjthlem1  25575  pjthlem2  25576  ivthlem3  25591  ivth2  25593  ovolfsf  25609  ovolsslem  25622  ovollb2lem  25626  ovollb2  25627  ovolctb  25628  ovolfiniun  25639  ovolicc1  25654  ovolicc2lem4  25658  ovolicc2  25660  nulmbl2  25674  unmbl  25675  ioombl1lem4  25699  uniioombllem4  25724  uniioombllem6  25726  volivth  25745  vitalilem4  25749  itg1ge0  25824  itg1ge0a  25849  itg1lea  25850  itg1climres  25852  mbfi1fseqlem5  25857  itg2ub  25871  itg2seq  25880  itg2uba  25881  itg2splitlem  25886  itg2split  25887  itg2monolem3  25890  itg2mono  25891  itg2i1fseq2  25894  itg2addlem  25896  iblss  25943  itggt0  25982  dvferm2lem  26124  dvlip  26131  dvivthlem1  26146  dvfsumlem2  26165  dvfsumlem3  26166  ftc1lem4  26177  ply1divmo  26272  ply1remlem  26301  fta1glem2  26305  idomrootle  26309  ig1pdvds  26316  plyeq0lem  26346  plydiveu  26438  fta1lem  26447  vieta1lem2  26451  aaliou3lem2  26483  aaliou3lem8  26485  ulmcn  26538  mtest  26543  itgulm  26547  radcnvlem1  26552  radcnvlt1  26557  dvradcnv  26560  pserdvlem2  26567  abelthlem2  26571  abelthlem6  26575  abelthlem7  26577  abelthlem9  26579  tangtx  26646  sinq12gt0  26648  sineq0  26665  cosordlem  26671  tanord  26679  tanregt0  26680  logrnaddcl  26715  logcj  26747  argregt0  26751  argrege0  26752  argimgt0  26753  argimlt0  26754  logimul  26755  logneg2  26756  logdivlti  26761  divlogrlim  26776  logcnlem3  26785  logcnlem4  26786  dvlog2lem  26793  logtayl  26801  rpcxpcl  26817  cxpsqrtlem  26843  cxpaddle  26893  isosctrlem1  26959  asinlem3a  27011  asinlem3  27012  asinneg  27027  asinsinlem  27032  asinsin  27033  atanlogaddlem  27054  atanlogadd  27055  atanlogsublem  27056  atanlogsub  27057  atantan  27064  atanbndlem  27066  atantayl  27078  leibpi  27083  birthdaylem3  27094  areaf  27102  cxploglim  27118  jensenlem2  27128  jensen  27129  logdiflbnd  27135  harmonicbnd4  27151  fsumharmonic  27152  zetacvg  27155  lgamgulmlem2  27170  lgamgulmlem3  27171  lgamcvg2  27195  wilthlem2  27209  wilthimp  27212  ftalem1  27213  ftalem2  27214  ftalem5  27217  basellem6  27226  basellem8  27228  basellem9  27229  chtge0  27252  chtublem  27351  logexprlim  27365  perfectlem1  27369  bcmax  27418  bposlem1  27424  bposlem2  27425  bposlem6  27429  bposlem7  27430  lgsdilem2  27473  lgsqrlem4  27489  lgsquadlem1  27520  2lgsoddprmlem2  27549  2sqlem3  27560  2sqlem8  27566  2sqblem  27571  2sqmod  27576  chebbnd1lem2  27610  chtppilimlem1  27613  chtppilim  27615  chto1ub  27616  vmadivsum  27622  rplogsumlem1  27624  rplogsumlem2  27625  dchrisum0lem1a  27626  rpvmasumlem  27627  dchrisumlem1  27629  dchrisumlem2  27630  dchrvmasumlem2  27638  dchrisum0flblem1  27648  dchrisum0flblem2  27649  dchrisum0lem1b  27655  dchrisum0lem1  27656  dchrisum0lem2a  27657  dchrisum0lem3  27659  dchrisum0  27660  mudivsum  27670  mulogsumlem  27671  mulog2sumlem1  27674  mulog2sumlem2  27675  2vmadivsumlem  27680  chpdifbndlem1  27693  selberg3lem1  27697  selberg4lem1  27700  pntrlog2bndlem1  27717  pntrlog2bndlem2  27718  pntrlog2bndlem3  27719  pntrlog2bndlem4  27720  pntpbnd1a  27725  pntpbnd1  27726  pntpbnd2  27727  pntibndlem2  27731  pntibndlem3  27732  pntlemd  27734  pntlemc  27735  pntlemb  27737  pntlemg  27738  pntlemh  27739  pntlemr  27742  pntlemf  27745  pntlemo  27747  abvcxp  27755  ostth2lem1  27758  padicabv  27770  ostth2lem2  27774  ostth2lem3  27775  ostth2lem4  27776  ostth2  27777  ostth3  27778  nodense  27832  nogt01o  27836  nosupbnd2lem1  27855  noetasuplem3  27875  maxs1  27909  maxs2  27910  eqcuts3  27973  cofcutr  28093  cofcutrtime  28096  addsuniflem  28170  negsunif  28224  sltmuls2  28317  precsexlem11  28386  abssge0  28414  leabss  28417  oncutlt  28433  om2noseqlt  28468  zsoring  28578  expsgt0  28606  halfcut  28627  addhalfcut  28628  bdayfinbndlem1  28636  elreno2  28664  tgcgr4  28776  legso  28844  krippenlem  28943  midex  28993  oppperpex  29009  prlngmid2  29183  ttgcontlem1  29200  axpaschlem  29256  axcontlem8  29287  upgrex  29408  nbfusgrlevtxm1  29693  finsumvtxdgeven  29868  wwlksnextproplem3  30226  clwlkclwwlk2  30320  clwlkclwwlkfolem  30324  clwwlkndivn  30397  ex-ind-dvds  30778  nvabs  30990  nmooge0  31085  nmoolb  31089  siii  31171  minvecolem2  31193  minvecolem4  31198  minvecolem5  31199  hlipgt0  31232  normge0  31444  normpyc  31464  pjhthlem1  31709  pjige0i  32008  nmoplb  32225  nmfnlb  32242  branmfn  32423  pjssdif2i  32492  stlei  32558  xlt2addrd  33070  eliccelico  33088  elicoelioo  33089  bcm1n  33106  fsumiunle  33139  nexple  33143  expevenpos  33145  pfxlsw2ccat  33236  wrdt2ind  33239  xrge0tsmsd  33359  gsumwrd2dccatlem  33363  psgnfzto1stlem  33386  cycpmco2lem4  33415  cycpmco2lem5  33416  cyc3conja  33443  archirngz  33475  archiabllem2c  33481  rprmasso2  33782  rprmirred  33787  1arithufdlem3  33802  vietadeg1  33934  lbslelsp  33954  fedgmullem2  33986  extdggt0  34013  evls1fldgencl  34026  fldextrspunlem1  34031  extdgfialglem1  34048  algextdeglem8  34080  rtelextdg2lem  34082  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  madjusmdetlem2  34184  locfinreflem  34196  xrge0iifiso  34291  gsumesum  34415  esumcst  34419  esumpcvgval  34434  esumcvg  34442  esumiun  34450  measssd  34571  measunl  34572  omssubadd  34656  carsgclctunlem3  34676  pmeasmono  34680  sibfof  34696  oddpwdc  34710  eulerpartlemgc  34718  iwrdsplit  34743  ballotlemsgt1  34867  ballotlemsel1i  34869  signsply0  34904  signstfvc  34927  signsvtp  34936  signsvfpn  34938  fdvposlt  34952  fdvneggt  34953  fdvnegge  34955  logdivsqrle  35003  hgt750lemf  35006  tgoldbachgtde  35013  swrdwlk  35573  subfaclim  35634  erdszelem7  35643  erdszelem8  35644  cvmliftlem2  35732  snmlff  35775  sinccvglem  36118  climlec3  36180  faclim  36192  fnejoin1  36823  poimirlem12  38227  poimirlem17  38232  poimirlem19  38234  poimirlem20  38235  poimirlem23  38238  poimirlem28  38243  broucube  38249  mblfinlem2  38253  mblfinlem3  38254  mblfinlem4  38255  ismblfin  38256  itg2addnclem  38266  itg2addnclem3  38268  itg2gt0cn  38270  itggt0cn  38285  ftc1anclem5  38292  ftc1anclem7  38294  ftc1anclem8  38295  isbnd3  38379  ssbnd  38383  heiborlem8  38413  bfplem2  38418  rrncmslem  38427  rrnequiv  38430  rrntotbnd  38431  lcv1  39761  lsatcv0eq  39767  lsatcvat3  39772  cvlsupr2  40063  hlatlej2  40096  cvrval4N  40134  cvratlem  40141  atcvr0eq  40146  2atlt  40159  atbtwnex  40168  athgt  40176  1cvrat  40196  ps-1  40197  hlatexch3N  40200  hlatexch4  40201  3atlem2  40204  atcvrlln2  40239  lplnexllnN  40284  4atlem3a  40317  4atlem10b  40325  4atlem11b  40328  4atlem12b  40331  2lplnja  40339  dalemply  40374  dalemsly  40375  dalem1  40379  dalem6  40388  dalem7  40389  dalem-cly  40391  dalem11  40394  dalem12  40395  dalem16  40399  dalem17  40400  dalem38  40430  dalem44  40436  dalem61  40453  lnatexN  40499  lncvrat  40502  lncmp  40503  paddasslem2  40541  dalawlem3  40593  dalawlem6  40596  dalawlem11  40601  lhpmcvr  40743  lhp2atne  40754  lhp2at0ne  40756  lautj  40813  trlval4  40908  cdlemc2  40912  cdlemc5  40915  cdleme3b  40949  cdleme11c  40981  cdleme19a  41023  cdleme20j  41038  cdleme22f  41066  cdleme23c  41071  cdleme26f2ALTN  41084  cdleme26f2  41085  cdleme35fnpq  41169  cdleme48bw  41222  cdlemg10a  41360  cdlemg11b  41362  cdlemg17g  41387  cdlemg18c  41400  cdlemi1  41538  cdlemk52  41674  dia2dimlem1  41784  dihord1  41938  dihjatcclem4  42141  lcmineqlem15  42756  lcmineqlem19  42760  lcmineqlem22  42763  aks4d1lem1  42775  aks4d1p1p4  42784  aks4d1p1p5  42788  aks4d1p2  42790  aks4d1p3  42791  aks4d1p6  42794  aks4d1p7d1  42795  aks4d1p7  42796  aks4d1p8  42800  aks4d1p9  42801  aks6d1c1p6  42827  aks6d1c1  42829  aks6d1c2  42843  sticksstones7  42865  aks6d1c7lem1  42893  unitscyglem4  42911  dvdsexpnn0  43041  prjspner01  43305  flt4lem5  43330  fltnltalem  43342  fltnlta  43343  3cubeslem1  43363  eldioph2lem1  43439  lzenom  43449  irrapxlem1  43497  irrapxlem4  43500  irrapxlem5  43501  pell14qrgt0  43534  pell1qrge1  43545  pell1qrgap  43549  pellfundge  43557  pellfundex  43561  pellfund14  43573  rmspecsqrtnq  43581  rmxypos  43622  ltrmynn0  43623  ltrmxnn0  43624  jm2.24nn  43634  jm2.17b  43636  jm2.17c  43637  jm2.24  43638  congadd  43641  congsym  43643  congneg  43644  congid  43646  mzpcong  43647  acongrep  43655  acongeq  43658  jm2.18  43663  jm2.19  43668  jm2.23  43671  jm2.25  43674  jm2.26lem3  43676  jm2.15nn0  43678  jm2.16nn0  43679  jm2.27a  43680  jm2.27c  43682  jm3.1lem1  43692  idomsubgmo  43868  sqrtcval  44315  inductionexd  44829  imo72b2lem0  44839  imo72b2  44846  dvgrat  44970  radcnvrat  44972  binomcxplemnn0  45007  binomcxplemnotnn0  45014  cncmpmax  45700  rnmptlb  45906  zltlesub  45952  infxrpnf  46108  xrpnf  46147  fmul01  46244  fmul01lt1lem1  46248  climdivf  46276  sumnnodd  46294  climinf2lem  46368  limsup10exlem  46434  climliminf  46468  dfxlim2v  46509  xlimliminflimsup  46524  dvdivbd  46585  volge0  46623  stoweidlem1  46663  stoweidlem16  46678  stoweidlem18  46680  stoweidlem24  46686  stoweidlem26  46688  stoweidlem36  46698  stoweidlem38  46700  stoweidlem41  46703  stoweidlem42  46704  stoweidlem44  46706  stoweidlem45  46707  stoweidlem48  46710  stoweidlem62  46724  wallispilem5  46731  stirlinglem1  46736  stirlinglem5  46740  stirlinglem7  46742  stirlinglem8  46743  stirlinglem9  46744  stirlinglem11  46746  fourierdlem4  46773  fourierdlem10  46779  fourierdlem37  46806  fourierdlem47  46815  fourierdlem72  46840  fourierdlem74  46842  fourierdlem79  46847  fourierdlem82  46850  fourierdlem89  46857  fourierdlem91  46859  fourierdlem93  46861  fourierdlem103  46871  fourierdlem104  46872  fourierdlem112  46880  etransclem24  46920  etransclem25  46921  etransclem28  46924  etransclem37  46933  etransclem38  46934  etransclem44  46940  meaiuninc3v  47146  vonicclem1  47345  pimconstlt0  47363  smfsuplem1  47473  chnerlem1  47546  rlimdmafv  47859  rlimdmafv2  47940  2elfz2melfz  48000  2timesltsq  48060  muldvdsfacgt  48068  iccpartgtprec  48114  iccpartlt  48118  iccpartgtl  48120  sqrtpwpw2p  48235  fmtnodvds  48241  goldbachthlem1  48242  lighneallem4a  48305  nprmdvdsfacm1lem1  48317  perfectALTVlem1  48431  uhgrimgrlim  48697  cznnring  48972  altgsumbcALT  49078  expnegico01  49243  flnn0div2ge  49258  rege1logbrege0  49283  fllogbd  49285  nnpw2blen  49305  nnolog2flm1  49315  dignn0ldlem  49327  dignn0flhalflem1  49340  dignn0flhalflem2  49341  eenglngeehlnmlem2  49463  itsclc0yqsol  49489  2itscp  49506  itscnhlinecirc02plem1  49507  itscnhlinecirc02plem2  49508  inlinecirc02p  49512