Theorem breqtrrd 5102

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

Syntax hints:   → wi 4   = wceq 1548   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075

This theorem is referenced by:  marypha1lem  9340  marypha2  9346  infsupprpr  9413  unxpwdom  9498  ttrcltr  9632  onadju  10111  nnadju  10115  cfss  10183  tskuni  10702  ltexnq  10894  lt2addmuld  12422  div4p1lem1div2  12427  nn0le2x  12486  mul2lt0rgt0  13042  prodge0ld  13047  ge2halflem1  13054  xrmax1  13122  xrmax2  13123  max1ALT  13133  qbtwnxr  13147  xleadd1a  13200  xlt2add  13207  xlesubadd  13210  xmulgt0  13230  xlemul1a  13235  xov1plusxeqvd  13446  uzsubsubfz  13495  fzctr  13589  subfzo0  13742  flflp1  13761  fldiv4lem1div2uz2  13790  ceilge  13799  modge0  13833  modlt  13834  modid  13850  m1modge3gt1  13875  modaddmodup  13891  sermono  13991  seqf1olem1  13998  seqf1olem2  13999  sqgt0  14083  sqge0  14093  leexp1a  14132  nnlesq  14162  expnbnd  14189  expmulnbnd  14192  discr1  14196  facwordi  14246  faclbnd5  14255  nfile  14316  hashdom  14336  hashgt23el  14381  fi1uzind  14464  brfi1indALT  14467  ccatdmss  14539  ccatws1n0  14590  swrds2  14897  cjmulge0  15103  resqrtcl  15210  absge0  15244  sqreulem  15317  amgm2  15327  rlimdm  15508  rlimge0  15538  reccn2  15554  climle  15597  climserle  15620  isercoll2  15626  iseraltlem1  15639  iseralt  15642  isumclim2  15715  isumclim3  15716  isumge0  15723  fsumless  15754  cvgcmp  15774  cvgcmpce  15776  abscvgcvg  15777  isumsup2  15806  isumltss  15808  climcndslem1  15809  climcnds  15811  supcvg  15816  harmonic  15819  expcnv  15824  explecnv  15825  cvgrat  15843  mertenslem1  15844  mertenslem2  15845  clim2div  15849  ntrivcvgtail  15860  iprodclim2  15959  iprodclim3  15960  efcvg  16045  ege2le3  16050  efaddlem  16053  eftlub  16071  effsumlt  16073  tanhlt1  16122  ef01bndlem  16146  sin02gt0  16154  rpnnen2lem4  16179  ruclem2  16194  ruclem3  16195  ruclem9  16200  iddvdsexp  16243  dvdsadd  16266  dvdsfac  16290  dvdsexp2im  16291  dvdsmod  16293  3dvds  16295  omoe  16328  sumeven  16351  divalglem1  16358  flodddiv4t2lthalf  16382  bitsfzo  16399  bitsmod  16400  bitscmp  16402  bitsinv1lem  16405  sadcaddlem  16421  sadadd3  16425  sadaddlem  16430  dvdssqim  16518  dvdsexpim  16519  dvdsmulgcd  16520  nn0seqcvgd  16534  dvdslcm  16562  lcmgcdlem  16570  dvdslcmf  16595  lcmfunsnlem2lem2  16603  mulgcddvds  16619  qredeq  16621  cncongr2  16632  sqnprm  16667  isprm6  16679  dvdszzq  16686  prmdvdsbc  16691  nonsq  16724  hashdvds  16740  prmdiv  16750  odzdvds  16761  pythagtriplem4  16785  pcpre1  16808  pcdvdsb  16835  pcz  16847  pcprmpw2  16848  pcaddlem  16854  pcadd  16855  pcadd2  16856  pcmpt  16858  pcmptdvds  16860  fldivp1  16863  pcfaclem  16864  pockthlem  16871  prmreclem1  16882  prmreclem3  16884  prmreclem5  16886  prmreclem6  16887  4sqlem6  16909  4sqlem8  16911  4sqlem11  16921  4sqlem12  16922  4sqlem14  16924  4sqlem16  16926  vdwlem3  16949  vdwlem9  16955  vdwlem10  16956  vdwlem12  16958  ramub1lem2  16993  prmgap  17025  prmgaplcm  17026  prmgapprmo  17028  mreexexd  17609  invfuc  17939  ple1  18389  chnub  18583  eqgen  19151  lagsubg  19165  pgpfi  19574  sylow2alem2  19587  sylow2a  19588  sylow3lem4  19599  efgsrel  19703  odadd1  19817  odadd2  19818  gexex  19822  lt6abl  19864  dprd2d2  20015  dmdprdpr  20020  ablfacrp2  20038  ablfac1c  20042  pgpfaclem1  20052  ablfac2  20060  fincygsubgodd  20083  omndmul2  20102  dvdsrmul1  20343  unitmulclb  20355  subrguss  20562  rhmsubcrngc  20643  abvres  20806  znfld  21538  znunit  21541  ofldchr  21554  frlmisfrlm  21826  ply1coefsupp  22286  evl1gsumadd  22347  matgsum  22423  pm2mpcl  22783  psmetxrge0  24299  isxmet2d  24313  mettri  24338  xmettri3  24339  mettri3  24340  xmetrtri2  24342  prdsxmetlem  24354  imasdsf1olem  24359  xblss2ps  24387  blss2ps  24389  blss2  24390  blssps  24410  blss  24411  prdsbl  24477  dscmet  24558  nmge0  24603  nmmtri  24608  tngngp3  24642  nlmvscnlem2  24671  nrginvrcnlem  24677  nmoix  24715  nmoleub  24717  blcvx  24784  xrsxmet  24796  opnreen  24818  xrge0tsms  24821  icopnfcnv  24930  xrhmeo  24934  lebnumii  24954  pcophtb  25017  pi1grplem  25037  nmoleub2lem  25102  ipcau2  25222  tcphcphlem1  25223  ipcau  25226  ipcnlem2  25232  rrxcph  25380  minveclem2  25414  minveclem3b  25416  pjthlem1  25425  pjthlem2  25426  ivthlem3  25441  ivth2  25443  ovolfsf  25459  ovolsslem  25472  ovollb2lem  25476  ovollb2  25477  ovolctb  25478  ovolfiniun  25489  ovolicc1  25504  ovolicc2lem4  25508  ovolicc2  25510  nulmbl2  25524  unmbl  25525  ioombl1lem4  25549  uniioombllem4  25574  uniioombllem6  25576  volivth  25595  vitalilem4  25599  itg1ge0  25674  itg1ge0a  25699  itg1lea  25700  itg1climres  25702  mbfi1fseqlem5  25707  itg2ub  25721  itg2seq  25730  itg2uba  25731  itg2splitlem  25736  itg2split  25737  itg2monolem3  25740  itg2mono  25741  itg2i1fseq2  25744  itg2addlem  25746  iblss  25793  itggt0  25832  dvferm2lem  25974  dvlip  25981  dvivthlem1  25996  dvfsumlem2  26015  dvfsumlem3  26016  ftc1lem4  26027  ply1divmo  26122  ply1remlem  26151  fta1glem2  26155  idomrootle  26159  ig1pdvds  26166  plyeq0lem  26196  plydiveu  26285  fta1lem  26294  vieta1lem2  26298  aaliou3lem2  26330  aaliou3lem8  26332  ulmcn  26385  mtest  26390  itgulm  26394  radcnvlem1  26399  radcnvlt1  26404  dvradcnv  26407  pserdvlem2  26414  abelthlem2  26418  abelthlem6  26422  abelthlem7  26424  abelthlem9  26426  tangtx  26490  sinq12gt0  26492  sineq0  26509  cosordlem  26515  tanord  26523  tanregt0  26524  logrnaddcl  26559  logcj  26591  argregt0  26595  argrege0  26596  argimgt0  26597  argimlt0  26598  logimul  26599  logneg2  26600  logdivlti  26605  divlogrlim  26620  logcnlem3  26629  logcnlem4  26630  dvlog2lem  26637  logtayl  26645  rpcxpcl  26661  cxpsqrtlem  26687  cxpaddle  26737  isosctrlem1  26803  asinlem3a  26855  asinlem3  26856  asinneg  26871  asinsinlem  26876  asinsin  26877  atanlogaddlem  26898  atanlogadd  26899  atanlogsublem  26900  atanlogsub  26901  atantan  26908  atanbndlem  26910  atantayl  26922  leibpi  26927  birthdaylem3  26938  areaf  26946  cxploglim  26962  jensenlem2  26972  jensen  26973  logdiflbnd  26979  harmonicbnd4  26995  fsumharmonic  26996  zetacvg  26999  lgamgulmlem2  27014  lgamgulmlem3  27015  lgamcvg2  27039  wilthlem2  27053  wilthimp  27056  ftalem1  27057  ftalem2  27058  ftalem5  27061  basellem6  27070  basellem8  27072  basellem9  27073  chtge0  27096  chtublem  27195  logexprlim  27209  perfectlem1  27213  bcmax  27262  bposlem1  27268  bposlem2  27269  bposlem6  27273  bposlem7  27274  lgsdilem2  27317  lgsqrlem4  27333  lgsquadlem1  27364  2lgsoddprmlem2  27393  2sqlem3  27404  2sqlem8  27410  2sqblem  27415  2sqmod  27420  chebbnd1lem2  27454  chtppilimlem1  27457  chtppilim  27459  chto1ub  27460  vmadivsum  27466  rplogsumlem1  27468  rplogsumlem2  27469  dchrisum0lem1a  27470  rpvmasumlem  27471  dchrisumlem1  27473  dchrisumlem2  27474  dchrvmasumlem2  27482  dchrisum0flblem1  27492  dchrisum0flblem2  27493  dchrisum0lem1b  27499  dchrisum0lem1  27500  dchrisum0lem2a  27501  dchrisum0lem3  27503  dchrisum0  27504  mudivsum  27514  mulogsumlem  27515  mulog2sumlem1  27518  mulog2sumlem2  27519  2vmadivsumlem  27524  chpdifbndlem1  27537  selberg3lem1  27541  selberg4lem1  27544  pntrlog2bndlem1  27561  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem4  27564  pntpbnd1a  27569  pntpbnd1  27570  pntpbnd2  27571  pntibndlem2  27575  pntibndlem3  27576  pntlemd  27578  pntlemc  27579  pntlemb  27581  pntlemg  27582  pntlemh  27583  pntlemr  27586  pntlemf  27589  pntlemo  27591  abvcxp  27599  ostth2lem1  27602  padicabv  27614  ostth2lem2  27618  ostth2lem3  27619  ostth2lem4  27620  ostth2  27621  ostth3  27622  nodense  27676  nogt01o  27680  nosupbnd2lem1  27699  noetasuplem3  27719  maxs1  27753  maxs2  27754  eqcuts3  27816  cofcutr  27936  cofcutrtime  27939  addsuniflem  28013  negsunif  28067  sltmuls2  28160  precsexlem11  28229  abssge0  28257  leabss  28260  oncutlt  28276  om2noseqlt  28311  zsoring  28421  expsgt0  28449  halfcut  28470  addhalfcut  28471  bdayfinbndlem1  28479  elreno2  28507  tgcgr4  28619  legso  28687  krippenlem  28778  midex  28825  oppperpex  28841  ttgcontlem1  28973  axpaschlem  29029  axcontlem8  29060  upgrex  29181  nbfusgrlevtxm1  29466  finsumvtxdgeven  29641  wwlksnextproplem3  29999  clwlkclwwlk2  30093  clwlkclwwlkfolem  30097  clwwlkndivn  30170  ex-ind-dvds  30551  nvabs  30763  nmooge0  30858  nmoolb  30862  siii  30944  minvecolem2  30966  minvecolem4  30971  minvecolem5  30972  hlipgt0  31005  normge0  31217  normpyc  31237  pjhthlem1  31482  pjige0i  31781  nmoplb  31998  nmfnlb  32015  branmfn  32196  pjssdif2i  32265  stlei  32331  xlt2addrd  32853  eliccelico  32871  elicoelioo  32872  bcm1n  32889  fsumiunle  32923  sgnmul  32929  nexple  32938  expevenpos  32940  pfxlsw2ccat  33031  wrdt2ind  33034  xrge0tsmsd  33156  gsumwrd2dccatlem  33160  psgnfzto1stlem  33183  cycpmco2lem4  33212  cycpmco2lem5  33213  cyc3conja  33240  archirngz  33272  archiabllem2c  33278  rprmasso2  33619  rprmirred  33624  1arithufdlem3  33639  vietadeg1  33772  lbslelsp  33792  fedgmullem2  33824  extdggt0  33851  evls1fldgencl  33864  fldextrspunlem1  33869  extdgfialglem1  33886  algextdeglem8  33918  rtelextdg2lem  33920  cos9thpiminplylem1  33976  cos9thpiminplylem2  33977  madjusmdetlem2  34022  locfinreflem  34034  xrge0iifiso  34129  gsumesum  34253  esumcst  34257  esumpcvgval  34272  esumcvg  34280  esumiun  34288  measssd  34409  measunl  34410  omssubadd  34494  carsgclctunlem3  34514  pmeasmono  34518  sibfof  34534  oddpwdc  34548  eulerpartlemgc  34556  iwrdsplit  34581  ballotlemsgt1  34705  ballotlemsel1i  34707  signsply0  34745  signstfvc  34768  signsvtp  34777  signsvfpn  34779  fdvposlt  34793  fdvneggt  34794  fdvnegge  34796  logdivsqrle  34844  hgt750lemf  34847  tgoldbachgtde  34854  swrdwlk  35368  subfaclim  35429  erdszelem7  35438  erdszelem8  35439  cvmliftlem2  35527  snmlff  35570  sinccvglem  35913  climlec3  35975  faclim  35987  fnejoin1  36609  poimirlem12  38012  poimirlem17  38017  poimirlem19  38019  poimirlem20  38020  poimirlem23  38023  poimirlem28  38028  broucube  38034  mblfinlem2  38038  mblfinlem3  38039  mblfinlem4  38040  ismblfin  38041  itg2addnclem  38051  itg2addnclem3  38053  itg2gt0cn  38055  itggt0cn  38070  ftc1anclem5  38077  ftc1anclem7  38079  ftc1anclem8  38080  isbnd3  38164  ssbnd  38168  heiborlem8  38198  bfplem2  38203  rrncmslem  38212  rrnequiv  38215  rrntotbnd  38216  lcv1  39546  lsatcv0eq  39552  lsatcvat3  39557  cvlsupr2  39848  hlatlej2  39881  cvrval4N  39919  cvratlem  39926  atcvr0eq  39931  2atlt  39944  atbtwnex  39953  athgt  39961  1cvrat  39981  ps-1  39982  hlatexch3N  39985  hlatexch4  39986  3atlem2  39989  atcvrlln2  40024  lplnexllnN  40069  4atlem3a  40102  4atlem10b  40110  4atlem11b  40113  4atlem12b  40116  2lplnja  40124  dalemply  40159  dalemsly  40160  dalem1  40164  dalem6  40173  dalem7  40174  dalem-cly  40176  dalem11  40179  dalem12  40180  dalem16  40184  dalem17  40185  dalem38  40215  dalem44  40221  dalem61  40238  lnatexN  40284  lncvrat  40287  lncmp  40288  paddasslem2  40326  dalawlem3  40378  dalawlem6  40381  dalawlem11  40386  lhpmcvr  40528  lhp2atne  40539  lhp2at0ne  40541  lautj  40598  trlval4  40693  cdlemc2  40697  cdlemc5  40700  cdleme3b  40734  cdleme11c  40766  cdleme19a  40808  cdleme20j  40823  cdleme22f  40851  cdleme23c  40856  cdleme26f2ALTN  40869  cdleme26f2  40870  cdleme35fnpq  40954  cdleme48bw  41007  cdlemg10a  41145  cdlemg11b  41147  cdlemg17g  41172  cdlemg18c  41185  cdlemi1  41323  cdlemk52  41459  dia2dimlem1  41569  dihord1  41723  dihjatcclem4  41926  lcmineqlem15  42541  lcmineqlem19  42545  lcmineqlem22  42548  aks4d1lem1  42560  aks4d1p1p4  42569  aks4d1p1p5  42573  aks4d1p2  42575  aks4d1p3  42576  aks4d1p6  42579  aks4d1p7d1  42580  aks4d1p7  42581  aks4d1p8  42585  aks4d1p9  42586  aks6d1c1p6  42612  aks6d1c1  42614  aks6d1c2  42628  sticksstones7  42650  aks6d1c7lem1  42678  unitscyglem4  42696  dvdsexpnn0  42824  prjspner01  43088  flt4lem5  43113  fltnltalem  43125  fltnlta  43126  3cubeslem1  43146  eldioph2lem1  43222  lzenom  43232  irrapxlem1  43280  irrapxlem4  43283  irrapxlem5  43284  pell14qrgt0  43317  pell1qrge1  43328  pell1qrgap  43332  pellfundge  43340  pellfundex  43344  pellfund14  43356  rmspecsqrtnq  43364  rmxypos  43405  ltrmynn0  43406  ltrmxnn0  43407  jm2.24nn  43417  jm2.17b  43419  jm2.17c  43420  jm2.24  43421  congadd  43424  congsym  43426  congneg  43427  congid  43429  mzpcong  43430  acongrep  43438  acongeq  43441  jm2.18  43446  jm2.19  43451  jm2.23  43454  jm2.25  43457  jm2.26lem3  43459  jm2.15nn0  43461  jm2.16nn0  43462  jm2.27a  43463  jm2.27c  43465  jm3.1lem1  43475  idomsubgmo  43651  sqrtcval  44098  inductionexd  44612  imo72b2lem0  44622  imo72b2  44629  dvgrat  44769  radcnvrat  44771  binomcxplemnn0  44806  binomcxplemnotnn0  44813  cncmpmax  45493  rnmptlb  45699  zltlesub  45745  infxrpnf  45901  xrpnf  45940  fmul01  46037  fmul01lt1lem1  46041  climdivf  46069  sumnnodd  46087  climinf2lem  46161  limsup10exlem  46227  climliminf  46261  dfxlim2v  46302  xlimliminflimsup  46317  dvdivbd  46378  volge0  46416  stoweidlem1  46456  stoweidlem16  46471  stoweidlem18  46473  stoweidlem24  46479  stoweidlem26  46481  stoweidlem36  46491  stoweidlem38  46493  stoweidlem41  46496  stoweidlem42  46497  stoweidlem44  46499  stoweidlem45  46500  stoweidlem48  46503  stoweidlem62  46517  wallispilem5  46524  stirlinglem1  46529  stirlinglem5  46533  stirlinglem7  46535  stirlinglem8  46536  stirlinglem9  46537  stirlinglem11  46539  fourierdlem4  46566  fourierdlem10  46572  fourierdlem37  46599  fourierdlem47  46608  fourierdlem72  46633  fourierdlem74  46635  fourierdlem79  46640  fourierdlem82  46643  fourierdlem89  46650  fourierdlem91  46652  fourierdlem93  46654  fourierdlem103  46664  fourierdlem104  46665  fourierdlem112  46673  etransclem24  46713  etransclem25  46714  etransclem28  46717  etransclem37  46726  etransclem38  46727  etransclem44  46733  meaiuninc3v  46939  vonicclem1  47138  pimconstlt0  47156  smfsuplem1  47266  chnerlem1  47339  rlimdmafv  47652  rlimdmafv2  47733  2elfz2melfz  47793  2timesltsq  47853  muldvdsfacgt  47861  iccpartgtprec  47907  iccpartlt  47911  iccpartgtl  47913  sqrtpwpw2p  48028  fmtnodvds  48034  goldbachthlem1  48035  lighneallem4a  48098  nprmdvdsfacm1lem1  48110  perfectALTVlem1  48224  uhgrimgrlim  48490  cznnring  48765  altgsumbcALT  48856  expnegico01  49021  flnn0div2ge  49036  rege1logbrege0  49061  fllogbd  49063  nnpw2blen  49083  nnolog2flm1  49093  dignn0ldlem  49105  dignn0flhalflem1  49118  dignn0flhalflem2  49119  eenglngeehlnmlem2  49241  itsclc0yqsol  49267  2itscp  49284  itscnhlinecirc02plem1  49285  itscnhlinecirc02plem2  49286  inlinecirc02p  49290