Theorem breqtrrd 5132

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  marypha1lem  9425  marypha2  9431  infsupprpr  9498  unxpwdom  9583  ttrcltr  9717  onadju  10272  nnadju  10276  cfss  10343  tskuni  10868  ltexnq  11060  lt2addmuld  12596  div4p1lem1div2  12601  nn0le2x  12660  mul2lt0rgt0  13225  prodge0ld  13230  ge2halflem1  13237  xrmax1  13305  xrmax2  13306  max1ALT  13316  qbtwnxr  13330  xleadd1a  13383  xlt2add  13390  xlesubadd  13393  xmulgt0  13413  xlemul1a  13418  xov1plusxeqvd  13629  uzsubsubfz  13680  fzctr  13774  subfzo0  13928  flflp1  13947  fldiv4lem1div2uz2  13976  ceilge  13985  modge0  14019  modlt  14020  modid  14036  m1modge3gt1  14061  modaddmodup  14077  sermono  14177  seqf1olem1  14184  seqf1olem2  14185  sqgt0  14269  sqge0  14279  leexp1a  14318  nnlesq  14349  expnbnd  14376  expmulnbnd  14379  discr1  14383  facwordi  14433  faclbnd5  14442  nfile  14503  hashdom  14523  hashgt23el  14569  fi1uzind  14652  brfi1indALT  14655  ccatdmss  14727  ccatws1n0  14780  swrds2  15091  sgnmul  15260  cjmulge0  15313  resqrtcl  15420  absge0  15454  sqreulem  15527  amgm2  15537  rlimdm  15718  rlimge0  15748  reccn2  15764  climle  15807  climserle  15830  isercoll2  15836  iseraltlem1  15849  iseralt  15852  isumclim2  15924  isumclim3  15925  isumge0  15932  fsumless  15963  cvgcmp  15983  cvgcmpce  15985  abscvgcvg  15986  isumsup2  16015  isumltss  16017  climcndslem1  16018  climcnds  16020  supcvg  16025  harmonic  16028  expcnv  16033  explecnv  16034  cvgrat  16052  mertenslem1  16053  mertenslem2  16054  clim2div  16058  ntrivcvgtail  16069  iprodclim2  16166  iprodclim3  16167  efcvg  16251  ege2le3  16256  efaddlem  16259  eftlub  16277  effsumlt  16279  tanhlt1  16328  ef01bndlem  16352  sin02gt0  16360  rpnnen2lem4  16385  ruclem2  16400  ruclem3  16401  ruclem9  16406  iddvdsexp  16449  dvdsadd  16472  dvdsfac  16496  dvdsexp2im  16497  dvdsmod  16499  3dvds  16501  omoe  16534  sumeven  16557  divalglem1  16564  flodddiv4t2lthalf  16588  bitsfzo  16605  bitsmod  16606  bitscmp  16608  bitsinv1lem  16611  sadcaddlem  16627  sadadd3  16631  sadaddlem  16636  dvdssqim  16727  dvdsexpim  16728  dvdsmulgcd  16730  nn0seqcvgd  16745  dvdslcm  16773  lcmgcdlem  16781  dvdslcmf  16806  lcmfunsnlem2lem2  16814  mulgcddvds  16830  qredeq  16832  cncongr2  16843  sqnprm  16878  isprm6  16890  dvdszzq  16897  prmdvdsbc  16902  nonsq  16935  hashdvds  16952  prmdiv  16962  odzdvds  16973  pythagtriplem4  16997  pcpre1  17020  pcdvdsb  17047  pcz  17059  pcprmpw2  17060  pcaddlem  17066  pcadd  17067  pcadd2  17068  pcmpt  17070  pcmptdvds  17072  fldivp1  17075  pcfaclem  17076  pockthlem  17083  prmreclem1  17094  prmreclem3  17096  prmreclem5  17098  prmreclem6  17099  4sqlem6  17121  4sqlem8  17123  4sqlem11  17133  4sqlem12  17134  4sqlem14  17136  4sqlem16  17138  vdwlem3  17161  vdwlem9  17167  vdwlem10  17168  vdwlem12  17170  ramub1lem2  17205  prmgap  17237  prmgaplcm  17238  prmgapprmo  17240  mreexexd  17822  invfuc  18152  ple1  18602  chnub  18796  eqgen  19393  lagsubg  19410  pgpfi  19819  sylow2alem2  19832  sylow2a  19833  sylow3lem4  19844  efgsrel  19948  odadd1  20062  odadd2  20063  gexex  20067  lt6abl  20109  dprd2d2  20260  dmdprdpr  20265  ablfacrp2  20283  ablfac1c  20287  pgpfaclem1  20297  ablfac2  20305  fincygsubgodd  20328  omndmul2  20347  dvdsrmul1  20599  unitmulclb  20611  subrguss  20839  rhmsubcrngc  20920  abvres  21088  znfld  21866  znunit  21869  ofldchr  21882  frlmisfrlm  22154  ply1coefsupp  22615  evl1gsumadd  22676  matgsum  22752  pm2mpcl  23115  psmetxrge0  24632  isxmet2d  24646  mettri  24671  xmettri3  24672  mettri3  24673  xmetrtri2  24675  prdsxmetlem  24687  imasdsf1olem  24692  xblss2ps  24720  blss2ps  24722  blss2  24723  blssps  24743  blss  24744  prdsbl  24810  dscmet  24891  nmge0  24936  nmmtri  24941  tngngp3  24975  nlmvscnlem2  25004  nrginvrcnlem  25010  nmoix  25048  nmoleub  25050  blcvx  25117  xrsxmet  25129  opnreen  25151  xrge0tsms  25154  icopnfcnv  25263  xrhmeo  25267  lebnumii  25287  pcophtb  25350  pi1grplem  25370  nmoleub2lem  25435  ipcau2  25555  tcphcphlem1  25556  ipcau  25559  ipcnlem2  25565  rrxcph  25713  minveclem2  25747  minveclem3b  25749  pjthlem1  25758  pjthlem2  25759  ivthlem3  25774  ivth2  25776  ovolfsf  25792  ovolsslem  25805  ovollb2lem  25809  ovollb2  25810  ovolctb  25811  ovolfiniun  25822  ovolicc1  25837  ovolicc2lem4  25841  ovolicc2  25843  nulmbl2  25857  unmbl  25858  ioombl1lem4  25882  uniioombllem4  25907  uniioombllem6  25909  volivth  25928  vitalilem4  25932  itg1ge0  26007  itg1ge0a  26032  itg1lea  26033  itg1climres  26035  mbfi1fseqlem5  26040  itg2ub  26054  itg2seq  26063  itg2uba  26064  itg2splitlem  26069  itg2split  26070  itg2monolem3  26073  itg2mono  26074  itg2i1fseq2  26077  itg2addlem  26079  iblss  26125  itggt0  26164  dvferm2lem  26306  dvlip  26313  dvivthlem1  26328  dvfsumlem2  26347  dvfsumlem3  26348  ftc1lem4  26359  ply1divmo  26454  ply1remlem  26483  fta1glem2  26487  idomrootle  26491  ig1pdvds  26498  plyeq0lem  26529  plydiveu  26619  fta1lem  26628  vieta1lem2  26634  aaliou3lem2  26670  aaliou3lem8  26672  ulmcn  26726  mtest  26731  itgulm  26735  radcnvlem1  26740  radcnvlt1  26745  dvradcnv  26748  pserdvlem2  26755  abelthlem2  26759  abelthlem6  26763  abelthlem7  26765  abelthlem9  26767  tangtx  26834  sinq12gt0  26836  sineq0  26852  cosordlem  26858  tanord  26866  tanregt0  26867  logrnaddcl  26902  logcj  26934  argregt0  26938  argrege0  26939  argimgt0  26940  argimlt0  26941  logimul  26942  logneg2  26943  logdivlti  26948  divlogrlim  26963  logcnlem3  26972  logcnlem4  26973  dvlog2lem  26980  logtayl  26988  rpcxpcl  27004  cxpsqrtlem  27030  cxpaddle  27080  isosctrlem1  27146  asinlem3a  27198  asinlem3  27199  asinneg  27214  asinsinlem  27219  asinsin  27220  atanlogaddlem  27241  atanlogadd  27242  atanlogsublem  27243  atanlogsub  27244  atantan  27251  atanbndlem  27253  atantayl  27265  leibpi  27270  birthdaylem3  27281  areaf  27289  cxploglim  27305  jensenlem2  27315  jensen  27316  logdiflbnd  27322  harmonicbnd4  27338  fsumharmonic  27339  zetacvg  27342  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamcvg2  27382  wilthlem2  27396  wilthimp  27399  ftalem1  27400  ftalem2  27401  ftalem5  27404  basellem6  27413  basellem8  27415  basellem9  27416  chtge0  27439  chtublem  27538  logexprlim  27552  perfectlem1  27556  bcmax  27605  bposlem1  27611  bposlem2  27612  bposlem6  27616  bposlem7  27617  lgsdilem2  27660  lgsqrlem4  27676  lgsquadlem1  27707  2lgsoddprmlem2  27736  2sqlem3  27747  2sqlem8  27753  2sqblem  27758  2sqmod  27763  chebbnd1lem2  27797  chtppilimlem1  27800  chtppilim  27802  chto1ub  27803  vmadivsum  27809  rplogsumlem1  27811  rplogsumlem2  27812  dchrisum0lem1a  27813  rpvmasumlem  27814  dchrisumlem1  27816  dchrisumlem2  27817  dchrvmasumlem2  27825  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem3  27846  dchrisum0  27847  mudivsum  27857  mulogsumlem  27858  mulog2sumlem1  27861  mulog2sumlem2  27862  2vmadivsumlem  27867  chpdifbndlem1  27880  selberg3lem1  27884  selberg4lem1  27887  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntibndlem2  27918  pntibndlem3  27919  pntlemd  27921  pntlemc  27922  pntlemb  27924  pntlemg  27925  pntlemh  27926  pntlemr  27929  pntlemf  27932  pntlemo  27934  abvcxp  27942  ostth2lem1  27945  padicabv  27957  ostth2lem2  27961  ostth2lem3  27962  ostth2lem4  27963  ostth2  27964  ostth3  27965  flt4lem5  27980  nodense  28049  nogt01o  28053  nosupbnd2lem1  28072  noetasuplem3  28092  maxs1  28126  maxs2  28127  eqcuts3  28190  cofcutr  28310  cofcutrtime  28313  addsuniflem  28387  negsunif  28441  sltmuls2  28534  precsexlem11  28603  abssge0  28631  leabss  28634  oncutlt  28650  om2noseqlt  28685  zsoring  28795  expsgt0  28823  halfcut  28844  addhalfcut  28845  bdayfinbndlem1  28853  elreno2  28881  tgcgr4  28994  legso  29062  krippenlem  29162  midex  29213  oppperpex  29229  angmgmaddcpbl  29390  angmgmaddlid  29392  angmgmaddrid  29393  prlngmid2  29439  prlngsymquadopp  29443  quadcgrprlng  29444  ttgcontlem1  29462  axpaschlem  29518  axcontlem8  29549  upgrex  29670  nbfusgrlevtxm1  29958  finsumvtxdgeven  30133  swrdwlk  30268  wwlksnextproplem3  30500  clwlkclwwlk2  30594  clwlkclwwlkfolem  30598  clwwlkndivn  30671  ex-ind-dvds  31062  nvabs  31274  nmooge0  31369  nmoolb  31373  siii  31455  minvecolem2  31477  minvecolem4  31482  minvecolem5  31483  hlipgt0  31516  normge0  31728  normpyc  31748  pjhthlem1  31993  pjige0i  32292  nmoplb  32509  nmfnlb  32526  branmfn  32707  pjssdif2i  32776  stlei  32842  xlt2addrd  33351  eliccelico  33369  elicoelioo  33370  bcm1n  33387  fsumiunle  33420  nexple  33424  expevenpos  33426  pfxlsw2ccat  33513  wrdt2ind  33516  xrge0tsmsd  33634  gsumwrd2dccatlem  33638  psgnfzto1stlem  33661  cycpmco2lem4  33690  cycpmco2lem5  33691  cyc3conja  33718  archirngz  33750  archiabllem2c  33756  rprmasso2  34058  rprmirred  34063  1arithufdlem3  34078  vietadeg1  34210  lbslelsp  34230  fedgmullem2  34262  extdggt0  34289  evls1fldgencl  34302  fldextrspunlem1  34307  extdgfialglem1  34324  algextdeglem8  34356  rtelextdg2lem  34358  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  madjusmdetlem2  34460  locfinreflem  34472  xrge0iifiso  34567  gsumesum  34691  esumcst  34695  esumpcvgval  34710  esumcvg  34718  esumiun  34726  measssd  34848  measunl  34849  omssubadd  34932  carsgclctunlem3  34952  pmeasmono  34956  sibfof  34972  oddpwdc  34986  eulerpartlemgc  34994  iwrdsplit  35019  ballotlemsgt1  35143  ballotlemsel1i  35145  signsply0  35180  signstfvc  35203  signsvtp  35212  signsvfpn  35214  fdvposlt  35228  fdvneggt  35229  fdvnegge  35231  logdivsqrle  35279  hgt750lemf  35282  tgoldbachgtde  35289  subfaclim  35953  erdszelem7  35962  erdszelem8  35963  cvmliftlem2  36051  snmlff  36094  sinccvglem  36437  climlec3  36499  faclim  36511  fnejoin1  37156  poimirlem12  38551  poimirlem17  38556  poimirlem19  38558  poimirlem20  38559  poimirlem23  38562  poimirlem28  38567  broucube  38573  mblfinlem2  38577  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  itg2addnclem  38590  itg2addnclem3  38592  itg2gt0cn  38594  itggt0cn  38609  ftc1anclem5  38616  ftc1anclem7  38618  ftc1anclem8  38619  isbnd3  38719  ssbnd  38723  heiborlem8  38753  bfplem2  38758  rrncmslem  38767  rrnequiv  38770  rrntotbnd  38771  lcv1  40099  lsatcv0eq  40105  lsatcvat3  40110  cvlsupr2  40401  hlatlej2  40434  cvrval4N  40472  cvratlem  40479  atcvr0eq  40484  2atlt  40497  atbtwnex  40506  athgt  40514  1cvrat  40534  ps-1  40535  hlatexch3N  40538  hlatexch4  40539  3atlem2  40542  atcvrlln2  40577  lplnexllnN  40622  4atlem3a  40655  4atlem10b  40663  4atlem11b  40666  4atlem12b  40669  2lplnja  40677  dalemply  40712  dalemsly  40713  dalem1  40717  dalem6  40726  dalem7  40727  dalem-cly  40729  dalem11  40732  dalem12  40733  dalem16  40737  dalem17  40738  dalem38  40768  dalem44  40774  dalem61  40791  lnatexN  40837  lncvrat  40840  lncmp  40841  paddasslem2  40879  dalawlem3  40931  dalawlem6  40934  dalawlem11  40939  lhpmcvr  41081  lhp2atne  41092  lhp2at0ne  41094  lautj  41151  trlval4  41246  cdlemc2  41250  cdlemc5  41253  cdleme3b  41287  cdleme11c  41319  cdleme19a  41361  cdleme20j  41376  cdleme22f  41404  cdleme23c  41409  cdleme26f2ALTN  41422  cdleme26f2  41423  cdleme35fnpq  41507  cdleme48bw  41560  cdlemg10a  41698  cdlemg11b  41700  cdlemg17g  41725  cdlemg18c  41738  cdlemi1  41876  cdlemk52  42012  dia2dimlem1  42122  dihord1  42276  dihjatcclem4  42479  lcmineqlem15  43094  lcmineqlem19  43098  lcmineqlem22  43101  aks4d1lem1  43113  aks4d1p1p4  43122  aks4d1p1p5  43126  aks4d1p2  43128  aks4d1p3  43129  aks4d1p6  43132  aks4d1p7d1  43133  aks4d1p7  43134  aks4d1p8  43138  aks4d1p9  43139  aks6d1c1p6  43165  aks6d1c1  43167  aks6d1c2  43181  sticksstones7  43203  aks6d1c7lem1  43231  unitscyglem4  43249  dvdsexpnn0  43387  prjspnequivnorm  43661  prjspnnorm  43662  fltnltalem  43674  fltnlta  43675  3cubeslem1  43695  eldioph2lem1  43771  lzenom  43781  irrapxlem1  43829  irrapxlem4  43832  irrapxlem5  43833  pell14qrgt0  43866  pell1qrge1  43877  pell1qrgap  43881  pellfundge  43889  pellfundex  43893  pellfund14  43905  rmspecsqrtnq  43913  rmxypos  43954  ltrmynn0  43955  ltrmxnn0  43956  jm2.24nn  43966  jm2.17b  43968  jm2.17c  43969  jm2.24  43970  congadd  43973  congsym  43975  congneg  43976  congid  43978  mzpcong  43979  acongrep  43987  acongeq  43990  jm2.18  43995  jm2.19  44000  jm2.23  44003  jm2.25  44006  jm2.26lem3  44008  jm2.15nn0  44010  jm2.16nn0  44011  jm2.27a  44012  jm2.27c  44014  jm3.1lem1  44024  idomsubgmo  44195  sqrtcval  44641  inductionexd  45155  imo72b2lem0  45165  imo72b2  45172  dvgrat  45296  radcnvrat  45298  binomcxplemnn0  45333  binomcxplemnotnn0  45340  cncmpmax  46049  rnmptlb  46255  zltlesub  46301  infxrpnf  46456  xrpnf  46495  fmul01  46592  fmul01lt1lem1  46596  climdivf  46624  sumnnodd  46642  climinf2lem  46716  limsup10exlem  46782  climliminf  46816  dfxlim2v  46857  xlimliminflimsup  46872  dvdivbd  46933  volge0  46971  stoweidlem1  47011  stoweidlem16  47026  stoweidlem18  47028  stoweidlem24  47034  stoweidlem26  47036  stoweidlem36  47046  stoweidlem38  47048  stoweidlem41  47051  stoweidlem42  47052  stoweidlem44  47054  stoweidlem45  47055  stoweidlem48  47058  stoweidlem62  47072  wallispilem5  47079  stirlinglem1  47084  stirlinglem5  47088  stirlinglem7  47090  stirlinglem8  47091  stirlinglem9  47092  stirlinglem11  47094  fourierdlem4  47121  fourierdlem10  47127  fourierdlem37  47154  fourierdlem47  47163  fourierdlem72  47188  fourierdlem74  47190  fourierdlem79  47195  fourierdlem82  47198  fourierdlem89  47205  fourierdlem91  47207  fourierdlem93  47209  fourierdlem103  47219  fourierdlem104  47220  fourierdlem112  47228  etransclem24  47268  etransclem25  47269  etransclem28  47272  etransclem37  47281  etransclem38  47282  etransclem44  47288  meaiuninc3v  47494  vonicclem1  47693  pimconstlt0  47711  smfsuplem1  47821  chnerlem1  47892  rlimdmafv  48247  rlimdmafv2  48328  2elfz2melfz  48388  2timesltsq  48448  muldvdsfacgt  48456  iccpartgtprec  48502  iccpartlt  48506  iccpartgtl  48508  sqrtpwpw2p  48623  fmtnodvds  48629  goldbachthlem1  48630  lighneallem4a  48693  nprmdvdsfacm1lem1  48705  perfectALTVlem1  48819  uhgrimgrlim  49085  cznnring  49359  altgsumbcALT  49465  expnegico01  49630  flnn0div2ge  49645  rege1logbrege0  49670  fllogbd  49672  nnpw2blen  49692  nnolog2flm1  49702  dignn0ldlem  49714  dignn0flhalflem1  49727  dignn0flhalflem2  49728  eenglngeehlnmlem2  49850  itsclc0yqsol  49876  2itscp  49893  itscnhlinecirc02plem1  49894  itscnhlinecirc02plem2  49895  inlinecirc02p  49899