Theorem breqtrrd 5137

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  marypha1lem  9406  marypha2  9412  infsupprpr  9479  unxpwdom  9564  ttrcltr  9698  onadju  10199  nnadju  10203  cfss  10270  tskuni  10795  ltexnq  10987  lt2addmuld  12521  div4p1lem1div2  12526  nn0le2x  12585  mul2lt0rgt0  13149  prodge0ld  13154  ge2halflem1  13161  xrmax1  13229  xrmax2  13230  max1ALT  13240  qbtwnxr  13254  xleadd1a  13307  xlt2add  13314  xlesubadd  13317  xmulgt0  13337  xlemul1a  13342  xov1plusxeqvd  13553  uzsubsubfz  13603  fzctr  13697  subfzo0  13851  flflp1  13870  fldiv4lem1div2uz2  13899  ceilge  13908  modge0  13942  modlt  13943  modid  13959  m1modge3gt1  13984  modaddmodup  14000  sermono  14100  seqf1olem1  14107  seqf1olem2  14108  sqgt0  14192  sqge0  14202  leexp1a  14241  nnlesq  14271  expnbnd  14298  expmulnbnd  14301  discr1  14305  facwordi  14355  faclbnd5  14364  nfile  14425  hashdom  14445  hashgt23el  14491  fi1uzind  14574  brfi1indALT  14577  ccatdmss  14649  ccatws1n0  14702  swrds2  15013  sgnmul  15182  cjmulge0  15235  resqrtcl  15342  absge0  15376  sqreulem  15449  amgm2  15459  rlimdm  15640  rlimge0  15670  reccn2  15686  climle  15729  climserle  15752  isercoll2  15758  iseraltlem1  15771  iseralt  15774  isumclim2  15846  isumclim3  15847  isumge0  15854  fsumless  15885  cvgcmp  15905  cvgcmpce  15907  abscvgcvg  15908  isumsup2  15937  isumltss  15939  climcndslem1  15940  climcnds  15942  supcvg  15947  harmonic  15950  expcnv  15955  explecnv  15956  cvgrat  15974  mertenslem1  15975  mertenslem2  15976  clim2div  15980  ntrivcvgtail  15991  iprodclim2  16090  iprodclim3  16091  efcvg  16175  ege2le3  16180  efaddlem  16183  eftlub  16201  effsumlt  16203  tanhlt1  16252  ef01bndlem  16276  sin02gt0  16284  rpnnen2lem4  16309  ruclem2  16324  ruclem3  16325  ruclem9  16330  iddvdsexp  16373  dvdsadd  16396  dvdsfac  16420  dvdsexp2im  16421  dvdsmod  16423  3dvds  16425  omoe  16458  sumeven  16481  divalglem1  16488  flodddiv4t2lthalf  16512  bitsfzo  16529  bitsmod  16530  bitscmp  16532  bitsinv1lem  16535  sadcaddlem  16551  sadadd3  16555  sadaddlem  16560  dvdssqim  16648  dvdsexpim  16649  dvdsmulgcd  16650  nn0seqcvgd  16664  dvdslcm  16692  lcmgcdlem  16700  dvdslcmf  16725  lcmfunsnlem2lem2  16733  mulgcddvds  16749  qredeq  16751  cncongr2  16762  sqnprm  16797  isprm6  16809  dvdszzq  16816  prmdvdsbc  16821  nonsq  16854  hashdvds  16870  prmdiv  16880  odzdvds  16891  pythagtriplem4  16915  pcpre1  16938  pcdvdsb  16965  pcz  16977  pcprmpw2  16978  pcaddlem  16984  pcadd  16985  pcadd2  16986  pcmpt  16988  pcmptdvds  16990  fldivp1  16993  pcfaclem  16994  pockthlem  17001  prmreclem1  17012  prmreclem3  17014  prmreclem5  17016  prmreclem6  17017  4sqlem6  17039  4sqlem8  17041  4sqlem11  17051  4sqlem12  17052  4sqlem14  17054  4sqlem16  17056  vdwlem3  17079  vdwlem9  17085  vdwlem10  17086  vdwlem12  17088  ramub1lem2  17123  prmgap  17155  prmgaplcm  17156  prmgapprmo  17158  mreexexd  17740  invfuc  18070  ple1  18520  chnub  18714  eqgen  19307  lagsubg  19324  pgpfi  19733  sylow2alem2  19746  sylow2a  19747  sylow3lem4  19758  efgsrel  19862  odadd1  19976  odadd2  19977  gexex  19981  lt6abl  20023  dprd2d2  20174  dmdprdpr  20179  ablfacrp2  20197  ablfac1c  20201  pgpfaclem1  20211  ablfac2  20219  fincygsubgodd  20242  omndmul2  20261  dvdsrmul1  20511  unitmulclb  20523  subrguss  20750  rhmsubcrngc  20831  abvres  20998  znfld  21774  znunit  21777  ofldchr  21790  frlmisfrlm  22062  ply1coefsupp  22523  evl1gsumadd  22584  matgsum  22660  pm2mpcl  23023  psmetxrge0  24540  isxmet2d  24554  mettri  24579  xmettri3  24580  mettri3  24581  xmetrtri2  24583  prdsxmetlem  24595  imasdsf1olem  24600  xblss2ps  24628  blss2ps  24630  blss2  24631  blssps  24651  blss  24652  prdsbl  24718  dscmet  24799  nmge0  24844  nmmtri  24849  tngngp3  24883  nlmvscnlem2  24912  nrginvrcnlem  24918  nmoix  24956  nmoleub  24958  blcvx  25025  xrsxmet  25037  opnreen  25059  xrge0tsms  25062  icopnfcnv  25171  xrhmeo  25175  lebnumii  25195  pcophtb  25258  pi1grplem  25278  nmoleub2lem  25343  ipcau2  25463  tcphcphlem1  25464  ipcau  25467  ipcnlem2  25473  rrxcph  25621  minveclem2  25655  minveclem3b  25657  pjthlem1  25666  pjthlem2  25667  ivthlem3  25682  ivth2  25684  ovolfsf  25700  ovolsslem  25713  ovollb2lem  25717  ovollb2  25718  ovolctb  25719  ovolfiniun  25730  ovolicc1  25745  ovolicc2lem4  25749  ovolicc2  25751  nulmbl2  25765  unmbl  25766  ioombl1lem4  25790  uniioombllem4  25815  uniioombllem6  25817  volivth  25836  vitalilem4  25840  itg1ge0  25915  itg1ge0a  25940  itg1lea  25941  itg1climres  25943  mbfi1fseqlem5  25948  itg2ub  25962  itg2seq  25971  itg2uba  25972  itg2splitlem  25977  itg2split  25978  itg2monolem3  25981  itg2mono  25982  itg2i1fseq2  25985  itg2addlem  25987  iblss  26034  itggt0  26073  dvferm2lem  26215  dvlip  26222  dvivthlem1  26237  dvfsumlem2  26256  dvfsumlem3  26257  ftc1lem4  26268  ply1divmo  26363  ply1remlem  26392  fta1glem2  26396  idomrootle  26400  ig1pdvds  26407  plyeq0lem  26437  plydiveu  26529  fta1lem  26538  vieta1lem2  26542  aaliou3lem2  26576  aaliou3lem8  26578  ulmcn  26632  mtest  26637  itgulm  26641  radcnvlem1  26646  radcnvlt1  26651  dvradcnv  26654  pserdvlem2  26661  abelthlem2  26665  abelthlem6  26669  abelthlem7  26671  abelthlem9  26673  tangtx  26740  sinq12gt0  26742  sineq0  26759  cosordlem  26765  tanord  26773  tanregt0  26774  logrnaddcl  26809  logcj  26841  argregt0  26845  argrege0  26846  argimgt0  26847  argimlt0  26848  logimul  26849  logneg2  26850  logdivlti  26855  divlogrlim  26870  logcnlem3  26879  logcnlem4  26880  dvlog2lem  26887  logtayl  26895  rpcxpcl  26911  cxpsqrtlem  26937  cxpaddle  26987  isosctrlem1  27053  asinlem3a  27105  asinlem3  27106  asinneg  27121  asinsinlem  27126  asinsin  27127  atanlogaddlem  27148  atanlogadd  27149  atanlogsublem  27150  atanlogsub  27151  atantan  27158  atanbndlem  27160  atantayl  27172  leibpi  27177  birthdaylem3  27188  areaf  27196  cxploglim  27212  jensenlem2  27222  jensen  27223  logdiflbnd  27229  harmonicbnd4  27245  fsumharmonic  27246  zetacvg  27249  lgamgulmlem2  27264  lgamgulmlem3  27265  lgamcvg2  27289  wilthlem2  27303  wilthimp  27306  ftalem1  27307  ftalem2  27308  ftalem5  27311  basellem6  27320  basellem8  27322  basellem9  27323  chtge0  27346  chtublem  27445  logexprlim  27459  perfectlem1  27463  bcmax  27512  bposlem1  27518  bposlem2  27519  bposlem6  27523  bposlem7  27524  lgsdilem2  27567  lgsqrlem4  27583  lgsquadlem1  27614  2lgsoddprmlem2  27643  2sqlem3  27654  2sqlem8  27660  2sqblem  27665  2sqmod  27670  chebbnd1lem2  27704  chtppilimlem1  27707  chtppilim  27709  chto1ub  27710  vmadivsum  27716  rplogsumlem1  27718  rplogsumlem2  27719  dchrisum0lem1a  27720  rpvmasumlem  27721  dchrisumlem1  27723  dchrisumlem2  27724  dchrvmasumlem2  27732  dchrisum0flblem1  27742  dchrisum0flblem2  27743  dchrisum0lem1b  27749  dchrisum0lem1  27750  dchrisum0lem2a  27751  dchrisum0lem3  27753  dchrisum0  27754  mudivsum  27764  mulogsumlem  27765  mulog2sumlem1  27768  mulog2sumlem2  27769  2vmadivsumlem  27774  chpdifbndlem1  27787  selberg3lem1  27791  selberg4lem1  27794  pntrlog2bndlem1  27811  pntrlog2bndlem2  27812  pntrlog2bndlem3  27813  pntrlog2bndlem4  27814  pntpbnd1a  27819  pntpbnd1  27820  pntpbnd2  27821  pntibndlem2  27825  pntibndlem3  27826  pntlemd  27828  pntlemc  27829  pntlemb  27831  pntlemg  27832  pntlemh  27833  pntlemr  27836  pntlemf  27839  pntlemo  27841  abvcxp  27849  ostth2lem1  27852  padicabv  27864  ostth2lem2  27868  ostth2lem3  27869  ostth2lem4  27870  ostth2  27871  ostth3  27872  nodense  27926  nogt01o  27930  nosupbnd2lem1  27949  noetasuplem3  27969  maxs1  28003  maxs2  28004  eqcuts3  28067  cofcutr  28187  cofcutrtime  28190  addsuniflem  28264  negsunif  28318  sltmuls2  28411  precsexlem11  28480  abssge0  28508  leabss  28511  oncutlt  28527  om2noseqlt  28562  zsoring  28672  expsgt0  28700  halfcut  28721  addhalfcut  28722  bdayfinbndlem1  28730  elreno2  28758  tgcgr4  28871  legso  28939  krippenlem  29039  midex  29090  oppperpex  29106  angmndaddcpbl  29263  prlngmid2  29304  prlngsymquadopp  29308  quadcgrprlng  29309  ttgcontlem1  29327  axpaschlem  29383  axcontlem8  29414  upgrex  29535  nbfusgrlevtxm1  29823  finsumvtxdgeven  29998  swrdwlk  30133  wwlksnextproplem3  30365  clwlkclwwlk2  30459  clwlkclwwlkfolem  30463  clwwlkndivn  30536  ex-ind-dvds  30927  nvabs  31139  nmooge0  31234  nmoolb  31238  siii  31320  minvecolem2  31342  minvecolem4  31347  minvecolem5  31348  hlipgt0  31381  normge0  31593  normpyc  31613  pjhthlem1  31858  pjige0i  32157  nmoplb  32374  nmfnlb  32391  branmfn  32572  pjssdif2i  32641  stlei  32707  xlt2addrd  33217  eliccelico  33235  elicoelioo  33236  bcm1n  33253  fsumiunle  33286  nexple  33290  expevenpos  33292  pfxlsw2ccat  33379  wrdt2ind  33382  xrge0tsmsd  33500  gsumwrd2dccatlem  33504  psgnfzto1stlem  33527  cycpmco2lem4  33556  cycpmco2lem5  33557  cyc3conja  33584  archirngz  33616  archiabllem2c  33622  rprmasso2  33923  rprmirred  33928  1arithufdlem3  33943  vietadeg1  34075  lbslelsp  34095  fedgmullem2  34127  extdggt0  34154  evls1fldgencl  34167  fldextrspunlem1  34172  extdgfialglem1  34189  algextdeglem8  34221  rtelextdg2lem  34223  cos9thpiminplylem1  34279  cos9thpiminplylem2  34280  madjusmdetlem2  34325  locfinreflem  34337  xrge0iifiso  34432  gsumesum  34556  esumcst  34560  esumpcvgval  34575  esumcvg  34583  esumiun  34591  measssd  34713  measunl  34714  omssubadd  34798  carsgclctunlem3  34818  pmeasmono  34822  sibfof  34838  oddpwdc  34852  eulerpartlemgc  34860  iwrdsplit  34885  ballotlemsgt1  35009  ballotlemsel1i  35011  signsply0  35046  signstfvc  35069  signsvtp  35078  signsvfpn  35080  fdvposlt  35094  fdvneggt  35095  fdvnegge  35097  logdivsqrle  35145  hgt750lemf  35148  tgoldbachgtde  35155  subfaclim  35754  erdszelem7  35763  erdszelem8  35764  cvmliftlem2  35852  snmlff  35895  sinccvglem  36238  climlec3  36300  faclim  36312  fnejoin1  36974  poimirlem12  38368  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem23  38379  poimirlem28  38384  broucube  38390  mblfinlem2  38394  mblfinlem3  38395  mblfinlem4  38396  ismblfin  38397  itg2addnclem  38407  itg2addnclem3  38409  itg2gt0cn  38411  itggt0cn  38426  ftc1anclem5  38433  ftc1anclem7  38435  ftc1anclem8  38436  isbnd3  38521  ssbnd  38525  heiborlem8  38555  bfplem2  38560  rrncmslem  38569  rrnequiv  38572  rrntotbnd  38573  lcv1  39901  lsatcv0eq  39907  lsatcvat3  39912  cvlsupr2  40203  hlatlej2  40236  cvrval4N  40274  cvratlem  40281  atcvr0eq  40286  2atlt  40299  atbtwnex  40308  athgt  40316  1cvrat  40336  ps-1  40337  hlatexch3N  40340  hlatexch4  40341  3atlem2  40344  atcvrlln2  40379  lplnexllnN  40424  4atlem3a  40457  4atlem10b  40465  4atlem11b  40468  4atlem12b  40471  2lplnja  40479  dalemply  40514  dalemsly  40515  dalem1  40519  dalem6  40528  dalem7  40529  dalem-cly  40531  dalem11  40534  dalem12  40535  dalem16  40539  dalem17  40540  dalem38  40570  dalem44  40576  dalem61  40593  lnatexN  40639  lncvrat  40642  lncmp  40643  paddasslem2  40681  dalawlem3  40733  dalawlem6  40736  dalawlem11  40741  lhpmcvr  40883  lhp2atne  40894  lhp2at0ne  40896  lautj  40953  trlval4  41048  cdlemc2  41052  cdlemc5  41055  cdleme3b  41089  cdleme11c  41121  cdleme19a  41163  cdleme20j  41178  cdleme22f  41206  cdleme23c  41211  cdleme26f2ALTN  41224  cdleme26f2  41225  cdleme35fnpq  41309  cdleme48bw  41362  cdlemg10a  41500  cdlemg11b  41502  cdlemg17g  41527  cdlemg18c  41540  cdlemi1  41678  cdlemk52  41814  dia2dimlem1  41924  dihord1  42078  dihjatcclem4  42281  lcmineqlem15  42896  lcmineqlem19  42900  lcmineqlem22  42903  aks4d1lem1  42915  aks4d1p1p4  42924  aks4d1p1p5  42928  aks4d1p2  42930  aks4d1p3  42931  aks4d1p6  42934  aks4d1p7d1  42935  aks4d1p7  42936  aks4d1p8  42940  aks4d1p9  42941  aks6d1c1p6  42967  aks6d1c1  42969  aks6d1c2  42983  sticksstones7  43005  aks6d1c7lem1  43033  unitscyglem4  43051  dvdsexpnn0  43196  prjspner01  43458  flt4lem5  43483  fltnltalem  43495  fltnlta  43496  3cubeslem1  43516  eldioph2lem1  43592  lzenom  43602  irrapxlem1  43650  irrapxlem4  43653  irrapxlem5  43654  pell14qrgt0  43687  pell1qrge1  43698  pell1qrgap  43702  pellfundge  43710  pellfundex  43714  pellfund14  43726  rmspecsqrtnq  43734  rmxypos  43775  ltrmynn0  43776  ltrmxnn0  43777  jm2.24nn  43787  jm2.17b  43789  jm2.17c  43790  jm2.24  43791  congadd  43794  congsym  43796  congneg  43797  congid  43799  mzpcong  43800  acongrep  43808  acongeq  43811  jm2.18  43816  jm2.19  43821  jm2.23  43824  jm2.25  43827  jm2.26lem3  43829  jm2.15nn0  43831  jm2.16nn0  43832  jm2.27a  43833  jm2.27c  43835  jm3.1lem1  43845  idomsubgmo  44021  sqrtcval  44468  inductionexd  44982  imo72b2lem0  44992  imo72b2  44999  dvgrat  45123  radcnvrat  45125  binomcxplemnn0  45160  binomcxplemnotnn0  45167  cncmpmax  45853  rnmptlb  46059  zltlesub  46105  infxrpnf  46261  xrpnf  46300  fmul01  46397  fmul01lt1lem1  46401  climdivf  46429  sumnnodd  46447  climinf2lem  46521  limsup10exlem  46587  climliminf  46621  dfxlim2v  46662  xlimliminflimsup  46677  dvdivbd  46738  volge0  46776  stoweidlem1  46816  stoweidlem16  46831  stoweidlem18  46833  stoweidlem24  46839  stoweidlem26  46841  stoweidlem36  46851  stoweidlem38  46853  stoweidlem41  46856  stoweidlem42  46857  stoweidlem44  46859  stoweidlem45  46860  stoweidlem48  46863  stoweidlem62  46877  wallispilem5  46884  stirlinglem1  46889  stirlinglem5  46893  stirlinglem7  46895  stirlinglem8  46896  stirlinglem9  46897  stirlinglem11  46899  fourierdlem4  46926  fourierdlem10  46932  fourierdlem37  46959  fourierdlem47  46968  fourierdlem72  46993  fourierdlem74  46995  fourierdlem79  47000  fourierdlem82  47003  fourierdlem89  47010  fourierdlem91  47012  fourierdlem93  47014  fourierdlem103  47024  fourierdlem104  47025  fourierdlem112  47033  etransclem24  47073  etransclem25  47074  etransclem28  47077  etransclem37  47086  etransclem38  47087  etransclem44  47093  meaiuninc3v  47299  vonicclem1  47498  pimconstlt0  47516  smfsuplem1  47626  chnerlem1  47697  rlimdmafv  48052  rlimdmafv2  48133  2elfz2melfz  48193  2timesltsq  48253  muldvdsfacgt  48261  iccpartgtprec  48307  iccpartlt  48311  iccpartgtl  48313  sqrtpwpw2p  48428  fmtnodvds  48434  goldbachthlem1  48435  lighneallem4a  48498  nprmdvdsfacm1lem1  48510  perfectALTVlem1  48624  uhgrimgrlim  48890  cznnring  49164  altgsumbcALT  49270  expnegico01  49435  flnn0div2ge  49450  rege1logbrege0  49475  fllogbd  49477  nnpw2blen  49497  nnolog2flm1  49507  dignn0ldlem  49519  dignn0flhalflem1  49532  dignn0flhalflem2  49533  eenglngeehlnmlem2  49655  itsclc0yqsol  49681  2itscp  49698  itscnhlinecirc02plem1  49699  itscnhlinecirc02plem2  49700  inlinecirc02p  49704