Theorem breqtrrd 5106

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079

This theorem is referenced by:  marypha1lem  9153  marypha2  9159  infsupprpr  9224  unxpwdom  9309  ttrcltr  9435  onadju  9933  nnadju  9937  cfss  10005  tskuni  10523  ltexnq  10715  lt2addmuld  12206  div4p1lem1div2  12211  mul2lt0rgt0  12815  prodge0ld  12820  xrmax1  12891  xrmax2  12892  max1ALT  12902  qbtwnxr  12916  xleadd1a  12969  xlt2add  12976  xlesubadd  12979  xmulgt0  12999  xlemul1a  13004  xov1plusxeqvd  13212  uzsubsubfz  13260  fzctr  13350  subfzo0  13490  flflp1  13508  fldiv4lem1div2uz2  13537  ceilge  13546  modge0  13580  modlt  13581  modid  13597  m1modge3gt1  13619  modaddmodup  13635  sermono  13736  seqf1olem1  13743  seqf1olem2  13744  sqgt0  13826  sqge0  13836  leexp1a  13874  nnlesq  13903  expnbnd  13928  expmulnbnd  13931  discr1  13935  facwordi  13984  faclbnd5  13993  nfile  14055  hashdom  14075  hashgt23el  14120  fi1uzind  14192  brfi1indALT  14195  ccatws1n0  14323  swrds2  14634  cjmulge0  14838  resqrtcl  14946  absge0  14980  sqreulem  15052  amgm2  15062  rlimdm  15241  rlimge0  15271  reccn2  15287  climle  15330  climserle  15355  isercoll2  15361  iseraltlem1  15374  iseralt  15377  isumclim2  15451  isumclim3  15452  isumge0  15459  fsumless  15489  cvgcmp  15509  cvgcmpce  15511  abscvgcvg  15512  isumsup2  15539  isumltss  15541  climcndslem1  15542  climcnds  15544  supcvg  15549  harmonic  15552  expcnv  15557  explecnv  15558  cvgrat  15576  mertenslem1  15577  mertenslem2  15578  clim2div  15582  ntrivcvgtail  15593  iprodclim2  15690  iprodclim3  15691  efcvg  15775  ege2le3  15780  efaddlem  15783  eftlub  15799  effsumlt  15801  tanhlt1  15850  ef01bndlem  15874  sin02gt0  15882  rpnnen2lem4  15907  ruclem2  15922  ruclem3  15923  ruclem9  15928  iddvdsexp  15970  dvdsadd  15992  dvdsfac  16016  dvdsexp2im  16017  dvdsmod  16019  3dvds  16021  omoe  16054  sumeven  16077  divalglem1  16084  flodddiv4t2lthalf  16106  bitsfzo  16123  bitsmod  16124  bitscmp  16126  bitsinv1lem  16129  sadcaddlem  16145  sadadd3  16149  sadaddlem  16154  dvdssqim  16245  dvdsmulgcd  16246  nn0seqcvgd  16256  dvdslcm  16284  lcmgcdlem  16292  dvdslcmf  16317  lcmfunsnlem2lem2  16325  mulgcddvds  16341  qredeq  16343  cncongr2  16354  sqnprm  16388  isprm6  16400  nonsq  16444  hashdvds  16457  prmdiv  16467  odzdvds  16477  pythagtriplem4  16501  pcpre1  16524  pcdvdsb  16551  pcz  16563  pcprmpw2  16564  pcaddlem  16570  pcadd  16571  pcadd2  16572  pcmpt  16574  pcmptdvds  16576  fldivp1  16579  pcfaclem  16580  pockthlem  16587  prmreclem1  16598  prmreclem3  16600  prmreclem5  16602  prmreclem6  16603  4sqlem6  16625  4sqlem8  16627  4sqlem11  16637  4sqlem12  16638  4sqlem14  16640  4sqlem16  16642  vdwlem3  16665  vdwlem9  16671  vdwlem10  16672  vdwlem12  16674  ramub1lem2  16709  prmgap  16741  prmgaplcm  16742  prmgapprmo  16744  mreexexd  17338  invfuc  17673  ple1  18129  eqgen  18790  lagsubg  18799  pgpfi  19191  sylow2alem2  19204  sylow2a  19205  sylow3lem4  19216  efgsrel  19321  odadd1  19430  odadd2  19431  gexex  19435  lt6abl  19477  dprd2d2  19628  dmdprdpr  19633  ablfacrp2  19651  ablfac1c  19655  pgpfaclem1  19665  ablfac2  19673  fincygsubgodd  19696  dvdsrmul1  19876  unitmulclb  19888  subrguss  20020  abvres  20080  znfld  20749  znunit  20752  frlmisfrlm  21036  ply1coefsupp  21447  evl1gsumadd  21505  matgsum  21567  pm2mpcl  21927  psmetxrge0  23447  isxmet2d  23461  mettri  23486  xmettri3  23487  mettri3  23488  xmetrtri2  23490  prdsxmetlem  23502  imasdsf1olem  23507  xblss2ps  23535  blss2ps  23537  blss2  23538  blssps  23558  blss  23559  prdsbl  23628  dscmet  23709  nmge0  23754  nmmtri  23759  tngngp3  23801  nlmvscnlem2  23830  nrginvrcnlem  23836  nmoix  23874  nmoleub  23876  blcvx  23942  xrsxmet  23953  opnreen  23975  xrge0tsms  23978  icopnfcnv  24086  xrhmeo  24090  lebnumii  24110  pcophtb  24173  pi1grplem  24193  nmoleub2lem  24258  ipcau2  24379  tcphcphlem1  24380  ipcau  24383  ipcnlem2  24389  rrxcph  24537  minveclem2  24571  minveclem3b  24573  pjthlem1  24582  pjthlem2  24583  ivthlem3  24598  ivth2  24600  ovolfsf  24616  ovolsslem  24629  ovollb2lem  24633  ovollb2  24634  ovolctb  24635  ovolfiniun  24646  ovolicc1  24661  ovolicc2lem4  24665  ovolicc2  24667  nulmbl2  24681  unmbl  24682  ioombl1lem4  24706  uniioombllem4  24731  uniioombllem6  24733  volivth  24752  vitalilem4  24756  itg1ge0  24831  itg1ge0a  24857  itg1lea  24858  itg1climres  24860  mbfi1fseqlem5  24865  itg2ub  24879  itg2seq  24888  itg2uba  24889  itg2splitlem  24894  itg2split  24895  itg2monolem3  24898  itg2mono  24899  itg2i1fseq2  24902  itg2addlem  24904  iblss  24950  itggt0  24989  dvferm2lem  25131  dvlip  25138  dvivthlem1  25153  dvfsumlem2  25172  dvfsumlem3  25173  ftc1lem4  25184  ply1divmo  25281  ply1remlem  25308  fta1glem2  25312  ig1pdvds  25322  plyeq0lem  25352  plydiveu  25439  fta1lem  25448  vieta1lem2  25452  aaliou3lem2  25484  aaliou3lem8  25486  ulmcn  25539  mtest  25544  itgulm  25548  radcnvlem1  25553  radcnvlt1  25558  dvradcnv  25561  pserdvlem2  25568  abelthlem2  25572  abelthlem6  25576  abelthlem7  25578  abelthlem9  25580  tangtx  25643  sinq12gt0  25645  sineq0  25661  cosordlem  25667  tanord  25675  tanregt0  25676  logrnaddcl  25711  logcj  25742  argregt0  25746  argrege0  25747  argimgt0  25748  argimlt0  25749  logimul  25750  logneg2  25751  logdivlti  25756  divlogrlim  25771  logcnlem3  25780  logcnlem4  25781  dvlog2lem  25788  logtayl  25796  rpcxpcl  25812  cxpsqrtlem  25838  cxpaddle  25886  isosctrlem1  25949  asinlem3a  26001  asinlem3  26002  asinneg  26017  asinsinlem  26022  asinsin  26023  atanlogaddlem  26044  atanlogadd  26045  atanlogsublem  26046  atanlogsub  26047  atantan  26054  atanbndlem  26056  atantayl  26068  leibpi  26073  birthdaylem3  26084  areaf  26092  cxploglim  26108  jensenlem2  26118  jensen  26119  logdiflbnd  26125  harmonicbnd4  26141  fsumharmonic  26142  zetacvg  26145  lgamgulmlem2  26160  lgamgulmlem3  26161  lgamcvg2  26185  wilthlem2  26199  wilthimp  26202  ftalem1  26203  ftalem2  26204  ftalem5  26207  basellem6  26216  basellem8  26218  basellem9  26219  chtge0  26242  chtublem  26340  logexprlim  26354  perfectlem1  26358  bcmax  26407  bposlem1  26413  bposlem2  26414  bposlem6  26418  bposlem7  26419  lgsdilem2  26462  lgsqrlem4  26478  lgsquadlem1  26509  2lgsoddprmlem2  26538  2sqlem3  26549  2sqlem8  26555  2sqblem  26560  2sqmod  26565  chebbnd1lem2  26599  chtppilimlem1  26602  chtppilim  26604  chto1ub  26605  vmadivsum  26611  rplogsumlem1  26613  rplogsumlem2  26614  dchrisum0lem1a  26615  rpvmasumlem  26616  dchrisumlem1  26618  dchrisumlem2  26619  dchrvmasumlem2  26627  dchrisum0flblem1  26637  dchrisum0flblem2  26638  dchrisum0lem1b  26644  dchrisum0lem1  26645  dchrisum0lem2a  26646  dchrisum0lem3  26648  dchrisum0  26649  mudivsum  26659  mulogsumlem  26660  mulog2sumlem1  26663  mulog2sumlem2  26664  2vmadivsumlem  26669  chpdifbndlem1  26682  selberg3lem1  26686  selberg4lem1  26689  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem4  26709  pntpbnd1a  26714  pntpbnd1  26715  pntpbnd2  26716  pntibndlem2  26720  pntibndlem3  26721  pntlemd  26723  pntlemc  26724  pntlemb  26726  pntlemg  26727  pntlemh  26728  pntlemr  26731  pntlemf  26734  pntlemo  26736  abvcxp  26744  ostth2lem1  26747  padicabv  26759  ostth2lem2  26763  ostth2lem3  26764  ostth2lem4  26765  ostth2  26766  ostth3  26767  tgcgr4  26873  legso  26941  krippenlem  27032  midex  27079  oppperpex  27095  ttgcontlem1  27233  axpaschlem  27289  axcontlem8  27320  upgrex  27443  nbfusgrlevtxm1  27725  finsumvtxdgeven  27900  wwlksnextproplem3  28255  clwlkclwwlk2  28346  clwlkclwwlkfolem  28350  clwwlkndivn  28423  ex-ind-dvds  28804  nvabs  29013  nmooge0  29108  nmoolb  29112  siii  29194  minvecolem2  29216  minvecolem4  29221  minvecolem5  29222  hlipgt0  29255  normge0  29467  normpyc  29487  pjhthlem1  29732  pjige0i  30031  nmoplb  30248  nmfnlb  30265  branmfn  30446  pjssdif2i  30515  stlei  30581  xlt2addrd  31060  eliccelico  31077  elicoelioo  31078  bcm1n  31095  dvdszzq  31108  prmdvdsbc  31109  fsumiunle  31122  pfxlsw2ccat  31203  wrdt2ind  31204  xrge0tsmsd  31296  omndmul2  31317  psgnfzto1stlem  31346  cycpmco2lem4  31375  cycpmco2lem5  31376  cyc3conja  31403  archirngz  31422  archiabllem2c  31428  ofldchr  31492  fedgmullem2  31690  extdggt0  31711  madjusmdetlem2  31757  locfinreflem  31769  xrge0iifiso  31864  nexple  31956  gsumesum  32006  esumcst  32010  esumpcvgval  32025  esumcvg  32033  esumiun  32041  measssd  32162  measunl  32163  omssubadd  32246  carsgclctunlem3  32266  pmeasmono  32270  sibfof  32286  oddpwdc  32300  eulerpartlemgc  32308  iwrdsplit  32333  ballotlemsgt1  32456  ballotlemsel1i  32458  sgnmul  32488  signsply0  32509  signstfvc  32532  signsvtp  32541  signsvfpn  32543  fdvposlt  32558  fdvneggt  32559  fdvnegge  32561  logdivsqrle  32609  hgt750lemf  32612  tgoldbachgtde  32619  swrdwlk  33067  subfaclim  33129  erdszelem7  33138  erdszelem8  33139  cvmliftlem2  33227  snmlff  33270  sinccvglem  33609  climlec3  33678  faclim  33691  nodense  33874  nogt01o  33878  nosupbnd2lem1  33897  noetasuplem3  33917  cofcutr  34071  cofcutrtime  34072  fnejoin1  34536  poimirlem12  35768  poimirlem17  35773  poimirlem19  35775  poimirlem20  35776  poimirlem23  35779  poimirlem28  35784  broucube  35790  mblfinlem2  35794  mblfinlem3  35795  mblfinlem4  35796  ismblfin  35797  itg2addnclem  35807  itg2addnclem3  35809  itg2gt0cn  35811  itggt0cn  35826  ftc1anclem5  35833  ftc1anclem7  35835  ftc1anclem8  35836  isbnd3  35921  ssbnd  35925  heiborlem8  35955  bfplem2  35960  rrncmslem  35969  rrnequiv  35972  rrntotbnd  35973  lcv1  37034  lsatcv0eq  37040  lsatcvat3  37045  cvlsupr2  37336  hlatlej2  37369  cvrval4N  37407  cvratlem  37414  atcvr0eq  37419  2atlt  37432  atbtwnex  37441  athgt  37449  1cvrat  37469  ps-1  37470  hlatexch3N  37473  hlatexch4  37474  3atlem2  37477  atcvrlln2  37512  lplnexllnN  37557  4atlem3a  37590  4atlem10b  37598  4atlem11b  37601  4atlem12b  37604  2lplnja  37612  dalemply  37647  dalemsly  37648  dalem1  37652  dalem6  37661  dalem7  37662  dalem-cly  37664  dalem11  37667  dalem12  37668  dalem16  37672  dalem17  37673  dalem38  37703  dalem44  37709  dalem61  37726  lnatexN  37772  lncvrat  37775  lncmp  37776  paddasslem2  37814  dalawlem3  37866  dalawlem6  37869  dalawlem11  37874  lhpmcvr  38016  lhp2atne  38027  lhp2at0ne  38029  lautj  38086  trlval4  38181  cdlemc2  38185  cdlemc5  38188  cdleme3b  38222  cdleme11c  38254  cdleme19a  38296  cdleme20j  38311  cdleme22f  38339  cdleme23c  38344  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme35fnpq  38442  cdleme48bw  38495  cdlemg10a  38633  cdlemg11b  38635  cdlemg17g  38660  cdlemg18c  38673  cdlemi1  38811  cdlemk52  38947  dia2dimlem1  39057  dihord1  39211  dihjatcclem4  39414  lcmineqlem15  40031  lcmineqlem19  40035  lcmineqlem22  40038  aks4d1lem1  40050  aks4d1p1p4  40059  aks4d1p1p5  40063  aks4d1p2  40065  aks4d1p3  40066  aks4d1p6  40069  aks4d1p7d1  40070  aks4d1p7  40071  aks4d1p8  40075  aks4d1p9  40076  sticksstones7  40088  metakunt7  40111  metakunt15  40119  metakunt16  40120  2xp3dxp2ge1d  40142  dvdsexpim  40308  dvdsexpnn0  40321  prjspner01  40442  flt4lem5  40467  fltnltalem  40479  fltnlta  40480  3cubeslem1  40486  eldioph2lem1  40562  lzenom  40572  irrapxlem1  40624  irrapxlem4  40627  irrapxlem5  40628  pell14qrgt0  40661  pell1qrge1  40672  pell1qrgap  40676  pellfundge  40684  pellfundex  40688  pellfund14  40700  rmspecsqrtnq  40708  rmxypos  40749  ltrmynn0  40750  ltrmxnn0  40751  jm2.24nn  40761  jm2.17b  40763  jm2.17c  40764  jm2.24  40765  congadd  40768  congsym  40770  congneg  40771  congid  40773  mzpcong  40774  acongrep  40782  acongeq  40785  jm2.18  40790  jm2.19  40795  jm2.23  40798  jm2.25  40801  jm2.26lem3  40803  jm2.15nn0  40805  jm2.16nn0  40806  jm2.27a  40807  jm2.27c  40809  jm3.1lem1  40819  idomrootle  41000  idomsubgmo  41003  sqrtcval  41202  inductionexd  41718  imo72b2  41736  dvgrat  41883  radcnvrat  41885  binomcxplemnn0  41920  binomcxplemnotnn0  41927  cncmpmax  42528  rnmptlb  42741  zltlesub  42777  infxrpnf  42940  xrpnf  42980  fmul01  43075  fmul01lt1lem1  43079  climdivf  43107  sumnnodd  43125  climinf2lem  43201  limsup10exlem  43267  climliminf  43301  dfxlim2v  43342  xlimliminflimsup  43357  dvdivbd  43418  volge0  43456  stoweidlem1  43496  stoweidlem16  43511  stoweidlem18  43513  stoweidlem24  43519  stoweidlem26  43521  stoweidlem36  43531  stoweidlem38  43533  stoweidlem41  43536  stoweidlem42  43537  stoweidlem44  43539  stoweidlem45  43540  stoweidlem48  43543  stoweidlem62  43557  wallispilem5  43564  stirlinglem1  43569  stirlinglem5  43573  stirlinglem7  43575  stirlinglem8  43576  stirlinglem9  43577  stirlinglem11  43579  fourierdlem4  43606  fourierdlem10  43612  fourierdlem37  43639  fourierdlem47  43648  fourierdlem72  43673  fourierdlem74  43675  fourierdlem79  43680  fourierdlem82  43683  fourierdlem89  43690  fourierdlem91  43692  fourierdlem93  43694  fourierdlem103  43704  fourierdlem104  43705  fourierdlem112  43713  etransclem24  43753  etransclem25  43754  etransclem28  43757  etransclem37  43766  etransclem38  43767  etransclem44  43773  meaiuninc3v  43976  vonicclem1  44175  pimconstlt0  44192  smfsuplem1  44295  rlimdmafv  44620  rlimdmafv2  44701  2elfz2melfz  44762  iccpartgtprec  44824  iccpartlt  44828  iccpartgtl  44830  sqrtpwpw2p  44942  fmtnodvds  44948  goldbachthlem1  44949  lighneallem4a  45012  perfectALTVlem1  45125  cznnring  45466  rhmsubcrngc  45539  altgsumbcALT  45641  expnegico01  45811  flnn0div2ge  45831  rege1logbrege0  45856  fllogbd  45858  nnpw2blen  45878  nnolog2flm1  45888  dignn0ldlem  45900  dignn0flhalflem1  45913  dignn0flhalflem2  45914  eenglngeehlnmlem2  46036  itsclc0yqsol  46062  2itscp  46079  itscnhlinecirc02plem1  46080  itscnhlinecirc02plem2  46081  inlinecirc02p  46085