Theorem breqtrrd 5128

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  marypha1lem  9350  marypha2  9356  infsupprpr  9423  unxpwdom  9508  ttrcltr  9639  onadju  10118  nnadju  10122  cfss  10189  tskuni  10708  ltexnq  10900  lt2addmuld  12405  div4p1lem1div2  12410  nn0le2x  12469  mul2lt0rgt0  13024  prodge0ld  13029  ge2halflem1  13036  xrmax1  13104  xrmax2  13105  max1ALT  13115  qbtwnxr  13129  xleadd1a  13182  xlt2add  13189  xlesubadd  13192  xmulgt0  13212  xlemul1a  13217  xov1plusxeqvd  13428  uzsubsubfz  13476  fzctr  13570  subfzo0  13722  flflp1  13741  fldiv4lem1div2uz2  13770  ceilge  13779  modge0  13813  modlt  13814  modid  13830  m1modge3gt1  13855  modaddmodup  13871  sermono  13971  seqf1olem1  13978  seqf1olem2  13979  sqgt0  14063  sqge0  14073  leexp1a  14112  nnlesq  14142  expnbnd  14169  expmulnbnd  14172  discr1  14176  facwordi  14226  faclbnd5  14235  nfile  14296  hashdom  14316  hashgt23el  14361  fi1uzind  14444  brfi1indALT  14447  ccatdmss  14519  ccatws1n0  14570  swrds2  14877  cjmulge0  15083  resqrtcl  15190  absge0  15224  sqreulem  15297  amgm2  15307  rlimdm  15488  rlimge0  15518  reccn2  15534  climle  15577  climserle  15600  isercoll2  15606  iseraltlem1  15619  iseralt  15622  isumclim2  15695  isumclim3  15696  isumge0  15703  fsumless  15733  cvgcmp  15753  cvgcmpce  15755  abscvgcvg  15756  isumsup2  15783  isumltss  15785  climcndslem1  15786  climcnds  15788  supcvg  15793  harmonic  15796  expcnv  15801  explecnv  15802  cvgrat  15820  mertenslem1  15821  mertenslem2  15822  clim2div  15826  ntrivcvgtail  15837  iprodclim2  15936  iprodclim3  15937  efcvg  16022  ege2le3  16027  efaddlem  16030  eftlub  16048  effsumlt  16050  tanhlt1  16099  ef01bndlem  16123  sin02gt0  16131  rpnnen2lem4  16156  ruclem2  16171  ruclem3  16172  ruclem9  16177  iddvdsexp  16220  dvdsadd  16243  dvdsfac  16267  dvdsexp2im  16268  dvdsmod  16270  3dvds  16272  omoe  16305  sumeven  16328  divalglem1  16335  flodddiv4t2lthalf  16359  bitsfzo  16376  bitsmod  16377  bitscmp  16379  bitsinv1lem  16382  sadcaddlem  16398  sadadd3  16402  sadaddlem  16407  dvdssqim  16495  dvdsexpim  16496  dvdsmulgcd  16497  nn0seqcvgd  16511  dvdslcm  16539  lcmgcdlem  16547  dvdslcmf  16572  lcmfunsnlem2lem2  16580  mulgcddvds  16596  qredeq  16598  cncongr2  16609  sqnprm  16643  isprm6  16655  dvdszzq  16662  prmdvdsbc  16667  nonsq  16700  hashdvds  16716  prmdiv  16726  odzdvds  16737  pythagtriplem4  16761  pcpre1  16784  pcdvdsb  16811  pcz  16823  pcprmpw2  16824  pcaddlem  16830  pcadd  16831  pcadd2  16832  pcmpt  16834  pcmptdvds  16836  fldivp1  16839  pcfaclem  16840  pockthlem  16847  prmreclem1  16858  prmreclem3  16860  prmreclem5  16862  prmreclem6  16863  4sqlem6  16885  4sqlem8  16887  4sqlem11  16897  4sqlem12  16898  4sqlem14  16900  4sqlem16  16902  vdwlem3  16925  vdwlem9  16931  vdwlem10  16932  vdwlem12  16934  ramub1lem2  16969  prmgap  17001  prmgaplcm  17002  prmgapprmo  17004  mreexexd  17585  invfuc  17915  ple1  18365  chnub  18559  eqgen  19127  lagsubg  19141  pgpfi  19551  sylow2alem2  19564  sylow2a  19565  sylow3lem4  19576  efgsrel  19680  odadd1  19794  odadd2  19795  gexex  19799  lt6abl  19841  dprd2d2  19992  dmdprdpr  19997  ablfacrp2  20015  ablfac1c  20019  pgpfaclem1  20029  ablfac2  20037  fincygsubgodd  20060  omndmul2  20079  dvdsrmul1  20322  unitmulclb  20334  subrguss  20537  rhmsubcrngc  20618  abvres  20781  znfld  21532  znunit  21535  ofldchr  21548  frlmisfrlm  21820  ply1coefsupp  22258  evl1gsumadd  22319  matgsum  22398  pm2mpcl  22758  psmetxrge0  24274  isxmet2d  24288  mettri  24313  xmettri3  24314  mettri3  24315  xmetrtri2  24317  prdsxmetlem  24329  imasdsf1olem  24334  xblss2ps  24362  blss2ps  24364  blss2  24365  blssps  24385  blss  24386  prdsbl  24452  dscmet  24533  nmge0  24578  nmmtri  24583  tngngp3  24617  nlmvscnlem2  24646  nrginvrcnlem  24652  nmoix  24690  nmoleub  24692  blcvx  24759  xrsxmet  24771  opnreen  24793  xrge0tsms  24796  icopnfcnv  24913  xrhmeo  24917  lebnumii  24938  pcophtb  25002  pi1grplem  25022  nmoleub2lem  25087  ipcau2  25207  tcphcphlem1  25208  ipcau  25211  ipcnlem2  25217  rrxcph  25365  minveclem2  25399  minveclem3b  25401  pjthlem1  25410  pjthlem2  25411  ivthlem3  25427  ivth2  25429  ovolfsf  25445  ovolsslem  25458  ovollb2lem  25462  ovollb2  25463  ovolctb  25464  ovolfiniun  25475  ovolicc1  25490  ovolicc2lem4  25494  ovolicc2  25496  nulmbl2  25510  unmbl  25511  ioombl1lem4  25535  uniioombllem4  25560  uniioombllem6  25562  volivth  25581  vitalilem4  25585  itg1ge0  25660  itg1ge0a  25685  itg1lea  25686  itg1climres  25688  mbfi1fseqlem5  25693  itg2ub  25707  itg2seq  25716  itg2uba  25717  itg2splitlem  25722  itg2split  25723  itg2monolem3  25726  itg2mono  25727  itg2i1fseq2  25730  itg2addlem  25732  iblss  25779  itggt0  25818  dvferm2lem  25963  dvlip  25971  dvivthlem1  25986  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem3  26008  ftc1lem4  26019  ply1divmo  26114  ply1remlem  26143  fta1glem2  26147  idomrootle  26151  ig1pdvds  26158  plyeq0lem  26188  plydiveu  26279  fta1lem  26288  vieta1lem2  26292  aaliou3lem2  26324  aaliou3lem8  26326  ulmcn  26381  mtest  26386  itgulm  26390  radcnvlem1  26395  radcnvlt1  26400  dvradcnv  26403  pserdvlem2  26411  abelthlem2  26415  abelthlem6  26419  abelthlem7  26421  abelthlem9  26423  tangtx  26487  sinq12gt0  26489  sineq0  26506  cosordlem  26512  tanord  26520  tanregt0  26521  logrnaddcl  26556  logcj  26588  argregt0  26592  argrege0  26593  argimgt0  26594  argimlt0  26595  logimul  26596  logneg2  26597  logdivlti  26602  divlogrlim  26617  logcnlem3  26626  logcnlem4  26627  dvlog2lem  26634  logtayl  26642  rpcxpcl  26658  cxpsqrtlem  26684  cxpaddle  26735  isosctrlem1  26801  asinlem3a  26853  asinlem3  26854  asinneg  26869  asinsinlem  26874  asinsin  26875  atanlogaddlem  26896  atanlogadd  26897  atanlogsublem  26898  atanlogsub  26899  atantan  26906  atanbndlem  26908  atantayl  26920  leibpi  26925  birthdaylem3  26936  areaf  26944  cxploglim  26961  jensenlem2  26971  jensen  26972  logdiflbnd  26978  harmonicbnd4  26994  fsumharmonic  26995  zetacvg  26998  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamcvg2  27038  wilthlem2  27052  wilthimp  27055  ftalem1  27056  ftalem2  27057  ftalem5  27060  basellem6  27069  basellem8  27071  basellem9  27072  chtge0  27095  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  27677  nogt01o  27681  nosupbnd2lem1  27700  noetasuplem3  27720  maxs1  27754  maxs2  27755  eqcuts3  27817  cofcutr  27937  cofcutrtime  27940  addsuniflem  28014  negsunif  28068  sltmuls2  28161  precsexlem11  28230  abssge0  28258  leabss  28261  oncutlt  28277  om2noseqlt  28312  zsoring  28422  expsgt0  28450  halfcut  28471  addhalfcut  28472  bdayfinbndlem1  28480  elreno2  28508  tgcgr4  28621  legso  28689  krippenlem  28780  midex  28827  oppperpex  28843  ttgcontlem1  28975  axpaschlem  29031  axcontlem8  29062  upgrex  29183  nbfusgrlevtxm1  29468  finsumvtxdgeven  29644  wwlksnextproplem3  30002  clwlkclwwlk2  30096  clwlkclwwlkfolem  30100  clwwlkndivn  30173  ex-ind-dvds  30554  nvabs  30766  nmooge0  30861  nmoolb  30865  siii  30947  minvecolem2  30969  minvecolem4  30974  minvecolem5  30975  hlipgt0  31008  normge0  31220  normpyc  31240  pjhthlem1  31485  pjige0i  31784  nmoplb  32001  nmfnlb  32018  branmfn  32199  pjssdif2i  32268  stlei  32334  xlt2addrd  32856  eliccelico  32874  elicoelioo  32875  bcm1n  32892  fsumiunle  32927  sgnmul  32933  nexple  32942  expevenpos  32944  pfxlsw2ccat  33049  wrdt2ind  33052  xrge0tsmsd  33173  gsumwrd2dccatlem  33177  psgnfzto1stlem  33200  cycpmco2lem4  33229  cycpmco2lem5  33230  cyc3conja  33257  archirngz  33289  archiabllem2c  33295  rprmasso2  33625  rprmirred  33630  1arithufdlem3  33645  vietadeg1  33761  lbslelsp  33781  fedgmullem2  33814  extdggt0  33841  evls1fldgencl  33854  fldextrspunlem1  33859  extdgfialglem1  33876  algextdeglem8  33908  rtelextdg2lem  33910  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  madjusmdetlem2  34012  locfinreflem  34024  xrge0iifiso  34119  gsumesum  34243  esumcst  34247  esumpcvgval  34262  esumcvg  34270  esumiun  34278  measssd  34399  measunl  34400  omssubadd  34484  carsgclctunlem3  34504  pmeasmono  34508  sibfof  34524  oddpwdc  34538  eulerpartlemgc  34546  iwrdsplit  34571  ballotlemsgt1  34695  ballotlemsel1i  34697  signsply0  34735  signstfvc  34758  signsvtp  34767  signsvfpn  34769  fdvposlt  34783  fdvneggt  34784  fdvnegge  34786  logdivsqrle  34834  hgt750lemf  34837  tgoldbachgtde  34844  swrdwlk  35349  subfaclim  35410  erdszelem7  35419  erdszelem8  35420  cvmliftlem2  35508  snmlff  35551  sinccvglem  35894  climlec3  35956  faclim  35968  fnejoin1  36590  poimirlem12  37912  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem23  37923  poimirlem28  37928  broucube  37934  mblfinlem2  37938  mblfinlem3  37939  mblfinlem4  37940  ismblfin  37941  itg2addnclem  37951  itg2addnclem3  37953  itg2gt0cn  37955  itggt0cn  37970  ftc1anclem5  37977  ftc1anclem7  37979  ftc1anclem8  37980  isbnd3  38064  ssbnd  38068  heiborlem8  38098  bfplem2  38103  rrncmslem  38112  rrnequiv  38115  rrntotbnd  38116  lcv1  39446  lsatcv0eq  39452  lsatcvat3  39457  cvlsupr2  39748  hlatlej2  39781  cvrval4N  39819  cvratlem  39826  atcvr0eq  39831  2atlt  39844  atbtwnex  39853  athgt  39861  1cvrat  39881  ps-1  39882  hlatexch3N  39885  hlatexch4  39886  3atlem2  39889  atcvrlln2  39924  lplnexllnN  39969  4atlem3a  40002  4atlem10b  40010  4atlem11b  40013  4atlem12b  40016  2lplnja  40024  dalemply  40059  dalemsly  40060  dalem1  40064  dalem6  40073  dalem7  40074  dalem-cly  40076  dalem11  40079  dalem12  40080  dalem16  40084  dalem17  40085  dalem38  40115  dalem44  40121  dalem61  40138  lnatexN  40184  lncvrat  40187  lncmp  40188  paddasslem2  40226  dalawlem3  40278  dalawlem6  40281  dalawlem11  40286  lhpmcvr  40428  lhp2atne  40439  lhp2at0ne  40441  lautj  40498  trlval4  40593  cdlemc2  40597  cdlemc5  40600  cdleme3b  40634  cdleme11c  40666  cdleme19a  40708  cdleme20j  40723  cdleme22f  40751  cdleme23c  40756  cdleme26f2ALTN  40769  cdleme26f2  40770  cdleme35fnpq  40854  cdleme48bw  40907  cdlemg10a  41045  cdlemg11b  41047  cdlemg17g  41072  cdlemg18c  41085  cdlemi1  41223  cdlemk52  41359  dia2dimlem1  41469  dihord1  41623  dihjatcclem4  41826  lcmineqlem15  42442  lcmineqlem19  42446  lcmineqlem22  42449  aks4d1lem1  42461  aks4d1p1p4  42470  aks4d1p1p5  42474  aks4d1p2  42476  aks4d1p3  42477  aks4d1p6  42480  aks4d1p7d1  42481  aks4d1p7  42482  aks4d1p8  42486  aks4d1p9  42487  aks6d1c1p6  42513  aks6d1c1  42515  aks6d1c2  42529  sticksstones7  42551  aks6d1c7lem1  42579  unitscyglem4  42597  dvdsexpnn0  42733  prjspner01  43012  flt4lem5  43037  fltnltalem  43049  fltnlta  43050  3cubeslem1  43070  eldioph2lem1  43146  lzenom  43156  irrapxlem1  43208  irrapxlem4  43211  irrapxlem5  43212  pell14qrgt0  43245  pell1qrge1  43256  pell1qrgap  43260  pellfundge  43268  pellfundex  43272  pellfund14  43284  rmspecsqrtnq  43292  rmxypos  43333  ltrmynn0  43334  ltrmxnn0  43335  jm2.24nn  43345  jm2.17b  43347  jm2.17c  43348  jm2.24  43349  congadd  43352  congsym  43354  congneg  43355  congid  43357  mzpcong  43358  acongrep  43366  acongeq  43369  jm2.18  43374  jm2.19  43379  jm2.23  43382  jm2.25  43385  jm2.26lem3  43387  jm2.15nn0  43389  jm2.16nn0  43390  jm2.27a  43391  jm2.27c  43393  jm3.1lem1  43403  idomsubgmo  43579  sqrtcval  44026  inductionexd  44540  imo72b2lem0  44550  imo72b2  44557  dvgrat  44697  radcnvrat  44699  binomcxplemnn0  44734  binomcxplemnotnn0  44741  cncmpmax  45421  rnmptlb  45630  zltlesub  45676  infxrpnf  45833  xrpnf  45872  fmul01  45969  fmul01lt1lem1  45973  climdivf  46001  sumnnodd  46019  climinf2lem  46093  limsup10exlem  46159  climliminf  46193  dfxlim2v  46234  xlimliminflimsup  46249  dvdivbd  46310  volge0  46348  stoweidlem1  46388  stoweidlem16  46403  stoweidlem18  46405  stoweidlem24  46411  stoweidlem26  46413  stoweidlem36  46423  stoweidlem38  46425  stoweidlem41  46428  stoweidlem42  46429  stoweidlem44  46431  stoweidlem45  46432  stoweidlem48  46435  stoweidlem62  46449  wallispilem5  46456  stirlinglem1  46461  stirlinglem5  46465  stirlinglem7  46467  stirlinglem8  46468  stirlinglem9  46469  stirlinglem11  46471  fourierdlem4  46498  fourierdlem10  46504  fourierdlem37  46531  fourierdlem47  46540  fourierdlem72  46565  fourierdlem74  46567  fourierdlem79  46572  fourierdlem82  46575  fourierdlem89  46582  fourierdlem91  46584  fourierdlem93  46586  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  etransclem24  46645  etransclem25  46646  etransclem28  46649  etransclem37  46658  etransclem38  46659  etransclem44  46665  meaiuninc3v  46871  vonicclem1  47070  pimconstlt0  47088  smfsuplem1  47198  chnerlem1  47269  rlimdmafv  47566  rlimdmafv2  47647  2elfz2melfz  47707  iccpartgtprec  47809  iccpartlt  47813  iccpartgtl  47815  sqrtpwpw2p  47927  fmtnodvds  47933  goldbachthlem1  47934  lighneallem4a  47997  perfectALTVlem1  48110  uhgrimgrlim  48376  cznnring  48651  altgsumbcALT  48742  expnegico01  48907  flnn0div2ge  48922  rege1logbrege0  48947  fllogbd  48949  nnpw2blen  48969  nnolog2flm1  48979  dignn0ldlem  48991  dignn0flhalflem1  49004  dignn0flhalflem2  49005  eenglngeehlnmlem2  49127  itsclc0yqsol  49153  2itscp  49170  itscnhlinecirc02plem1  49171  itscnhlinecirc02plem2  49172  inlinecirc02p  49176