Theorem breqtrrd 5127

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 5125	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  marypha1lem  9340  marypha2  9346  infsupprpr  9413  unxpwdom  9498  ttrcltr  9629  onadju  10108  nnadju  10112  cfss  10179  tskuni  10698  ltexnq  10890  lt2addmuld  12395  div4p1lem1div2  12400  nn0le2x  12459  mul2lt0rgt0  13014  prodge0ld  13019  ge2halflem1  13026  xrmax1  13094  xrmax2  13095  max1ALT  13105  qbtwnxr  13119  xleadd1a  13172  xlt2add  13179  xlesubadd  13182  xmulgt0  13202  xlemul1a  13207  xov1plusxeqvd  13418  uzsubsubfz  13466  fzctr  13560  subfzo0  13712  flflp1  13731  fldiv4lem1div2uz2  13760  ceilge  13769  modge0  13803  modlt  13804  modid  13820  m1modge3gt1  13845  modaddmodup  13861  sermono  13961  seqf1olem1  13968  seqf1olem2  13969  sqgt0  14053  sqge0  14063  leexp1a  14102  nnlesq  14132  expnbnd  14159  expmulnbnd  14162  discr1  14166  facwordi  14216  faclbnd5  14225  nfile  14286  hashdom  14306  hashgt23el  14351  fi1uzind  14434  brfi1indALT  14437  ccatdmss  14509  ccatws1n0  14560  swrds2  14867  cjmulge0  15073  resqrtcl  15180  absge0  15214  sqreulem  15287  amgm2  15297  rlimdm  15478  rlimge0  15508  reccn2  15524  climle  15567  climserle  15590  isercoll2  15596  iseraltlem1  15609  iseralt  15612  isumclim2  15685  isumclim3  15686  isumge0  15693  fsumless  15723  cvgcmp  15743  cvgcmpce  15745  abscvgcvg  15746  isumsup2  15773  isumltss  15775  climcndslem1  15776  climcnds  15778  supcvg  15783  harmonic  15786  expcnv  15791  explecnv  15792  cvgrat  15810  mertenslem1  15811  mertenslem2  15812  clim2div  15816  ntrivcvgtail  15827  iprodclim2  15926  iprodclim3  15927  efcvg  16012  ege2le3  16017  efaddlem  16020  eftlub  16038  effsumlt  16040  tanhlt1  16089  ef01bndlem  16113  sin02gt0  16121  rpnnen2lem4  16146  ruclem2  16161  ruclem3  16162  ruclem9  16167  iddvdsexp  16210  dvdsadd  16233  dvdsfac  16257  dvdsexp2im  16258  dvdsmod  16260  3dvds  16262  omoe  16295  sumeven  16318  divalglem1  16325  flodddiv4t2lthalf  16349  bitsfzo  16366  bitsmod  16367  bitscmp  16369  bitsinv1lem  16372  sadcaddlem  16388  sadadd3  16392  sadaddlem  16397  dvdssqim  16485  dvdsexpim  16486  dvdsmulgcd  16487  nn0seqcvgd  16501  dvdslcm  16529  lcmgcdlem  16537  dvdslcmf  16562  lcmfunsnlem2lem2  16570  mulgcddvds  16586  qredeq  16588  cncongr2  16599  sqnprm  16633  isprm6  16645  dvdszzq  16652  prmdvdsbc  16657  nonsq  16690  hashdvds  16706  prmdiv  16716  odzdvds  16727  pythagtriplem4  16751  pcpre1  16774  pcdvdsb  16801  pcz  16813  pcprmpw2  16814  pcaddlem  16820  pcadd  16821  pcadd2  16822  pcmpt  16824  pcmptdvds  16826  fldivp1  16829  pcfaclem  16830  pockthlem  16837  prmreclem1  16848  prmreclem3  16850  prmreclem5  16852  prmreclem6  16853  4sqlem6  16875  4sqlem8  16877  4sqlem11  16887  4sqlem12  16888  4sqlem14  16890  4sqlem16  16892  vdwlem3  16915  vdwlem9  16921  vdwlem10  16922  vdwlem12  16924  ramub1lem2  16959  prmgap  16991  prmgaplcm  16992  prmgapprmo  16994  mreexexd  17575  invfuc  17905  ple1  18355  chnub  18549  eqgen  19114  lagsubg  19128  pgpfi  19538  sylow2alem2  19551  sylow2a  19552  sylow3lem4  19563  efgsrel  19667  odadd1  19781  odadd2  19782  gexex  19786  lt6abl  19828  dprd2d2  19979  dmdprdpr  19984  ablfacrp2  20002  ablfac1c  20006  pgpfaclem1  20016  ablfac2  20024  fincygsubgodd  20047  omndmul2  20066  dvdsrmul1  20309  unitmulclb  20321  subrguss  20524  rhmsubcrngc  20605  abvres  20768  znfld  21519  znunit  21522  ofldchr  21535  frlmisfrlm  21807  ply1coefsupp  22245  evl1gsumadd  22306  matgsum  22385  pm2mpcl  22745  psmetxrge0  24261  isxmet2d  24275  mettri  24300  xmettri3  24301  mettri3  24302  xmetrtri2  24304  prdsxmetlem  24316  imasdsf1olem  24321  xblss2ps  24349  blss2ps  24351  blss2  24352  blssps  24372  blss  24373  prdsbl  24439  dscmet  24520  nmge0  24565  nmmtri  24570  tngngp3  24604  nlmvscnlem2  24633  nrginvrcnlem  24639  nmoix  24677  nmoleub  24679  blcvx  24746  xrsxmet  24758  opnreen  24780  xrge0tsms  24783  icopnfcnv  24900  xrhmeo  24904  lebnumii  24925  pcophtb  24989  pi1grplem  25009  nmoleub2lem  25074  ipcau2  25194  tcphcphlem1  25195  ipcau  25198  ipcnlem2  25204  rrxcph  25352  minveclem2  25386  minveclem3b  25388  pjthlem1  25397  pjthlem2  25398  ivthlem3  25414  ivth2  25416  ovolfsf  25432  ovolsslem  25445  ovollb2lem  25449  ovollb2  25450  ovolctb  25451  ovolfiniun  25462  ovolicc1  25477  ovolicc2lem4  25481  ovolicc2  25483  nulmbl2  25497  unmbl  25498  ioombl1lem4  25522  uniioombllem4  25547  uniioombllem6  25549  volivth  25568  vitalilem4  25572  itg1ge0  25647  itg1ge0a  25672  itg1lea  25673  itg1climres  25675  mbfi1fseqlem5  25680  itg2ub  25694  itg2seq  25703  itg2uba  25704  itg2splitlem  25709  itg2split  25710  itg2monolem3  25713  itg2mono  25714  itg2i1fseq2  25717  itg2addlem  25719  iblss  25766  itggt0  25805  dvferm2lem  25950  dvlip  25958  dvivthlem1  25973  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem3  25995  ftc1lem4  26006  ply1divmo  26101  ply1remlem  26130  fta1glem2  26134  idomrootle  26138  ig1pdvds  26145  plyeq0lem  26175  plydiveu  26266  fta1lem  26275  vieta1lem2  26279  aaliou3lem2  26311  aaliou3lem8  26313  ulmcn  26368  mtest  26373  itgulm  26377  radcnvlem1  26382  radcnvlt1  26387  dvradcnv  26390  pserdvlem2  26398  abelthlem2  26402  abelthlem6  26406  abelthlem7  26408  abelthlem9  26410  tangtx  26474  sinq12gt0  26476  sineq0  26493  cosordlem  26499  tanord  26507  tanregt0  26508  logrnaddcl  26543  logcj  26575  argregt0  26579  argrege0  26580  argimgt0  26581  argimlt0  26582  logimul  26583  logneg2  26584  logdivlti  26589  divlogrlim  26604  logcnlem3  26613  logcnlem4  26614  dvlog2lem  26621  logtayl  26629  rpcxpcl  26645  cxpsqrtlem  26671  cxpaddle  26722  isosctrlem1  26788  asinlem3a  26840  asinlem3  26841  asinneg  26856  asinsinlem  26861  asinsin  26862  atanlogaddlem  26883  atanlogadd  26884  atanlogsublem  26885  atanlogsub  26886  atantan  26893  atanbndlem  26895  atantayl  26907  leibpi  26912  birthdaylem3  26923  areaf  26931  cxploglim  26948  jensenlem2  26958  jensen  26959  logdiflbnd  26965  harmonicbnd4  26981  fsumharmonic  26982  zetacvg  26985  lgamgulmlem2  27000  lgamgulmlem3  27001  lgamcvg2  27025  wilthlem2  27039  wilthimp  27042  ftalem1  27043  ftalem2  27044  ftalem5  27047  basellem6  27056  basellem8  27058  basellem9  27059  chtge0  27082  chtublem  27182  logexprlim  27196  perfectlem1  27200  bcmax  27249  bposlem1  27255  bposlem2  27256  bposlem6  27260  bposlem7  27261  lgsdilem2  27304  lgsqrlem4  27320  lgsquadlem1  27351  2lgsoddprmlem2  27380  2sqlem3  27391  2sqlem8  27397  2sqblem  27402  2sqmod  27407  chebbnd1lem2  27441  chtppilimlem1  27444  chtppilim  27446  chto1ub  27447  vmadivsum  27453  rplogsumlem1  27455  rplogsumlem2  27456  dchrisum0lem1a  27457  rpvmasumlem  27458  dchrisumlem1  27460  dchrisumlem2  27461  dchrvmasumlem2  27469  dchrisum0flblem1  27479  dchrisum0flblem2  27480  dchrisum0lem1b  27486  dchrisum0lem1  27487  dchrisum0lem2a  27488  dchrisum0lem3  27490  dchrisum0  27491  mudivsum  27501  mulogsumlem  27502  mulog2sumlem1  27505  mulog2sumlem2  27506  2vmadivsumlem  27511  chpdifbndlem1  27524  selberg3lem1  27528  selberg4lem1  27531  pntrlog2bndlem1  27548  pntrlog2bndlem2  27549  pntrlog2bndlem3  27550  pntrlog2bndlem4  27551  pntpbnd1a  27556  pntpbnd1  27557  pntpbnd2  27558  pntibndlem2  27562  pntibndlem3  27563  pntlemd  27565  pntlemc  27566  pntlemb  27568  pntlemg  27569  pntlemh  27570  pntlemr  27573  pntlemf  27576  pntlemo  27578  abvcxp  27586  ostth2lem1  27589  padicabv  27601  ostth2lem2  27605  ostth2lem3  27606  ostth2lem4  27607  ostth2  27608  ostth3  27609  nodense  27664  nogt01o  27668  nosupbnd2lem1  27687  noetasuplem3  27707  maxs1  27741  maxs2  27742  eqcuts3  27804  cofcutr  27924  cofcutrtime  27927  addsuniflem  28001  negsunif  28055  sltmuls2  28148  precsexlem11  28217  abssge0  28245  leabss  28248  oncutlt  28264  om2noseqlt  28299  zsoring  28409  expsgt0  28437  halfcut  28458  addhalfcut  28459  bdayfinbndlem1  28467  elreno2  28495  tgcgr4  28607  legso  28675  krippenlem  28766  midex  28813  oppperpex  28829  ttgcontlem1  28961  axpaschlem  29017  axcontlem8  29048  upgrex  29169  nbfusgrlevtxm1  29454  finsumvtxdgeven  29630  wwlksnextproplem3  29988  clwlkclwwlk2  30082  clwlkclwwlkfolem  30086  clwwlkndivn  30159  ex-ind-dvds  30540  nvabs  30751  nmooge0  30846  nmoolb  30850  siii  30932  minvecolem2  30954  minvecolem4  30959  minvecolem5  30960  hlipgt0  30993  normge0  31205  normpyc  31225  pjhthlem1  31470  pjige0i  31769  nmoplb  31986  nmfnlb  32003  branmfn  32184  pjssdif2i  32253  stlei  32319  xlt2addrd  32841  eliccelico  32859  elicoelioo  32860  bcm1n  32877  fsumiunle  32912  sgnmul  32918  nexple  32927  expevenpos  32929  pfxlsw2ccat  33034  wrdt2ind  33037  xrge0tsmsd  33157  gsumwrd2dccatlem  33161  psgnfzto1stlem  33184  cycpmco2lem4  33213  cycpmco2lem5  33214  cyc3conja  33241  archirngz  33273  archiabllem2c  33279  rprmasso2  33609  rprmirred  33614  1arithufdlem3  33629  vietadeg1  33736  lbslelsp  33756  fedgmullem2  33789  extdggt0  33816  evls1fldgencl  33829  fldextrspunlem1  33834  extdgfialglem1  33851  algextdeglem8  33883  rtelextdg2lem  33885  cos9thpiminplylem1  33941  cos9thpiminplylem2  33942  madjusmdetlem2  33987  locfinreflem  33999  xrge0iifiso  34094  gsumesum  34218  esumcst  34222  esumpcvgval  34237  esumcvg  34245  esumiun  34253  measssd  34374  measunl  34375  omssubadd  34459  carsgclctunlem3  34479  pmeasmono  34483  sibfof  34499  oddpwdc  34513  eulerpartlemgc  34521  iwrdsplit  34546  ballotlemsgt1  34670  ballotlemsel1i  34672  signsply0  34710  signstfvc  34733  signsvtp  34742  signsvfpn  34744  fdvposlt  34758  fdvneggt  34759  fdvnegge  34761  logdivsqrle  34809  hgt750lemf  34812  tgoldbachgtde  34819  swrdwlk  35323  subfaclim  35384  erdszelem7  35393  erdszelem8  35394  cvmliftlem2  35482  snmlff  35525  sinccvglem  35868  climlec3  35930  faclim  35942  fnejoin1  36564  poimirlem12  37835  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem23  37846  poimirlem28  37851  broucube  37857  mblfinlem2  37861  mblfinlem3  37862  mblfinlem4  37863  ismblfin  37864  itg2addnclem  37874  itg2addnclem3  37876  itg2gt0cn  37878  itggt0cn  37893  ftc1anclem5  37900  ftc1anclem7  37902  ftc1anclem8  37903  isbnd3  37987  ssbnd  37991  heiborlem8  38021  bfplem2  38026  rrncmslem  38035  rrnequiv  38038  rrntotbnd  38039  lcv1  39369  lsatcv0eq  39375  lsatcvat3  39380  cvlsupr2  39671  hlatlej2  39704  cvrval4N  39742  cvratlem  39749  atcvr0eq  39754  2atlt  39767  atbtwnex  39776  athgt  39784  1cvrat  39804  ps-1  39805  hlatexch3N  39808  hlatexch4  39809  3atlem2  39812  atcvrlln2  39847  lplnexllnN  39892  4atlem3a  39925  4atlem10b  39933  4atlem11b  39936  4atlem12b  39939  2lplnja  39947  dalemply  39982  dalemsly  39983  dalem1  39987  dalem6  39996  dalem7  39997  dalem-cly  39999  dalem11  40002  dalem12  40003  dalem16  40007  dalem17  40008  dalem38  40038  dalem44  40044  dalem61  40061  lnatexN  40107  lncvrat  40110  lncmp  40111  paddasslem2  40149  dalawlem3  40201  dalawlem6  40204  dalawlem11  40209  lhpmcvr  40351  lhp2atne  40362  lhp2at0ne  40364  lautj  40421  trlval4  40516  cdlemc2  40520  cdlemc5  40523  cdleme3b  40557  cdleme11c  40589  cdleme19a  40631  cdleme20j  40646  cdleme22f  40674  cdleme23c  40679  cdleme26f2ALTN  40692  cdleme26f2  40693  cdleme35fnpq  40777  cdleme48bw  40830  cdlemg10a  40968  cdlemg11b  40970  cdlemg17g  40995  cdlemg18c  41008  cdlemi1  41146  cdlemk52  41282  dia2dimlem1  41392  dihord1  41546  dihjatcclem4  41749  lcmineqlem15  42365  lcmineqlem19  42369  lcmineqlem22  42372  aks4d1lem1  42384  aks4d1p1p4  42393  aks4d1p1p5  42397  aks4d1p2  42399  aks4d1p3  42400  aks4d1p6  42403  aks4d1p7d1  42404  aks4d1p7  42405  aks4d1p8  42409  aks4d1p9  42410  aks6d1c1p6  42436  aks6d1c1  42438  aks6d1c2  42452  sticksstones7  42474  aks6d1c7lem1  42502  unitscyglem4  42520  dvdsexpnn0  42656  prjspner01  42935  flt4lem5  42960  fltnltalem  42972  fltnlta  42973  3cubeslem1  42993  eldioph2lem1  43069  lzenom  43079  irrapxlem1  43131  irrapxlem4  43134  irrapxlem5  43135  pell14qrgt0  43168  pell1qrge1  43179  pell1qrgap  43183  pellfundge  43191  pellfundex  43195  pellfund14  43207  rmspecsqrtnq  43215  rmxypos  43256  ltrmynn0  43257  ltrmxnn0  43258  jm2.24nn  43268  jm2.17b  43270  jm2.17c  43271  jm2.24  43272  congadd  43275  congsym  43277  congneg  43278  congid  43280  mzpcong  43281  acongrep  43289  acongeq  43292  jm2.18  43297  jm2.19  43302  jm2.23  43305  jm2.25  43308  jm2.26lem3  43310  jm2.15nn0  43312  jm2.16nn0  43313  jm2.27a  43314  jm2.27c  43316  jm3.1lem1  43326  idomsubgmo  43502  sqrtcval  43949  inductionexd  44463  imo72b2lem0  44473  imo72b2  44480  dvgrat  44620  radcnvrat  44622  binomcxplemnn0  44657  binomcxplemnotnn0  44664  cncmpmax  45344  rnmptlb  45554  zltlesub  45600  infxrpnf  45757  xrpnf  45796  fmul01  45893  fmul01lt1lem1  45897  climdivf  45925  sumnnodd  45943  climinf2lem  46017  limsup10exlem  46083  climliminf  46117  dfxlim2v  46158  xlimliminflimsup  46173  dvdivbd  46234  volge0  46272  stoweidlem1  46312  stoweidlem16  46327  stoweidlem18  46329  stoweidlem24  46335  stoweidlem26  46337  stoweidlem36  46347  stoweidlem38  46349  stoweidlem41  46352  stoweidlem42  46353  stoweidlem44  46355  stoweidlem45  46356  stoweidlem48  46359  stoweidlem62  46373  wallispilem5  46380  stirlinglem1  46385  stirlinglem5  46389  stirlinglem7  46391  stirlinglem8  46392  stirlinglem9  46393  stirlinglem11  46395  fourierdlem4  46422  fourierdlem10  46428  fourierdlem37  46455  fourierdlem47  46464  fourierdlem72  46489  fourierdlem74  46491  fourierdlem79  46496  fourierdlem82  46499  fourierdlem89  46506  fourierdlem91  46508  fourierdlem93  46510  fourierdlem103  46520  fourierdlem104  46521  fourierdlem112  46529  etransclem24  46569  etransclem25  46570  etransclem28  46573  etransclem37  46582  etransclem38  46583  etransclem44  46589  meaiuninc3v  46795  vonicclem1  46994  pimconstlt0  47012  smfsuplem1  47122  chnerlem1  47193  rlimdmafv  47490  rlimdmafv2  47571  2elfz2melfz  47631  iccpartgtprec  47733  iccpartlt  47737  iccpartgtl  47739  sqrtpwpw2p  47851  fmtnodvds  47857  goldbachthlem1  47858  lighneallem4a  47921  perfectALTVlem1  48034  uhgrimgrlim  48300  cznnring  48575  altgsumbcALT  48666  expnegico01  48831  flnn0div2ge  48846  rege1logbrege0  48871  fllogbd  48873  nnpw2blen  48893  nnolog2flm1  48903  dignn0ldlem  48915  dignn0flhalflem1  48928  dignn0flhalflem2  48929  eenglngeehlnmlem2  49051  itsclc0yqsol  49077  2itscp  49094  itscnhlinecirc02plem1  49095  itscnhlinecirc02plem2  49096  inlinecirc02p  49100