Theorem breqtrrd 5120

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-br 5093

This theorem is referenced by:  marypha1lem  9290  marypha2  9296  infsupprpr  9361  unxpwdom  9446  ttrcltr  9573  onadju  10050  nnadju  10054  cfss  10122  tskuni  10640  ltexnq  10832  lt2addmuld  12324  div4p1lem1div2  12329  mul2lt0rgt0  12934  prodge0ld  12939  xrmax1  13010  xrmax2  13011  max1ALT  13021  qbtwnxr  13035  xleadd1a  13088  xlt2add  13095  xlesubadd  13098  xmulgt0  13118  xlemul1a  13123  xov1plusxeqvd  13331  uzsubsubfz  13379  fzctr  13469  subfzo0  13610  flflp1  13628  fldiv4lem1div2uz2  13657  ceilge  13666  modge0  13700  modlt  13701  modid  13717  m1modge3gt1  13739  modaddmodup  13755  sermono  13856  seqf1olem1  13863  seqf1olem2  13864  sqgt0  13946  sqge0  13956  leexp1a  13994  nnlesq  14023  expnbnd  14048  expmulnbnd  14051  discr1  14055  facwordi  14104  faclbnd5  14113  nfile  14174  hashdom  14194  hashgt23el  14239  fi1uzind  14311  brfi1indALT  14314  ccatws1n0  14440  swrds2  14752  cjmulge0  14956  resqrtcl  15064  absge0  15098  sqreulem  15170  amgm2  15180  rlimdm  15359  rlimge0  15389  reccn2  15405  climle  15448  climserle  15473  isercoll2  15479  iseraltlem1  15492  iseralt  15495  isumclim2  15569  isumclim3  15570  isumge0  15577  fsumless  15607  cvgcmp  15627  cvgcmpce  15629  abscvgcvg  15630  isumsup2  15657  isumltss  15659  climcndslem1  15660  climcnds  15662  supcvg  15667  harmonic  15670  expcnv  15675  explecnv  15676  cvgrat  15694  mertenslem1  15695  mertenslem2  15696  clim2div  15700  ntrivcvgtail  15711  iprodclim2  15808  iprodclim3  15809  efcvg  15893  ege2le3  15898  efaddlem  15901  eftlub  15917  effsumlt  15919  tanhlt1  15968  ef01bndlem  15992  sin02gt0  16000  rpnnen2lem4  16025  ruclem2  16040  ruclem3  16041  ruclem9  16046  iddvdsexp  16088  dvdsadd  16110  dvdsfac  16134  dvdsexp2im  16135  dvdsmod  16137  3dvds  16139  omoe  16172  sumeven  16195  divalglem1  16202  flodddiv4t2lthalf  16224  bitsfzo  16241  bitsmod  16242  bitscmp  16244  bitsinv1lem  16247  sadcaddlem  16263  sadadd3  16267  sadaddlem  16272  dvdssqim  16361  dvdsmulgcd  16362  nn0seqcvgd  16372  dvdslcm  16400  lcmgcdlem  16408  dvdslcmf  16433  lcmfunsnlem2lem2  16441  mulgcddvds  16457  qredeq  16459  cncongr2  16470  sqnprm  16504  isprm6  16516  nonsq  16560  hashdvds  16573  prmdiv  16583  odzdvds  16593  pythagtriplem4  16617  pcpre1  16640  pcdvdsb  16667  pcz  16679  pcprmpw2  16680  pcaddlem  16686  pcadd  16687  pcadd2  16688  pcmpt  16690  pcmptdvds  16692  fldivp1  16695  pcfaclem  16696  pockthlem  16703  prmreclem1  16714  prmreclem3  16716  prmreclem5  16718  prmreclem6  16719  4sqlem6  16741  4sqlem8  16743  4sqlem11  16753  4sqlem12  16754  4sqlem14  16756  4sqlem16  16758  vdwlem3  16781  vdwlem9  16787  vdwlem10  16788  vdwlem12  16790  ramub1lem2  16825  prmgap  16857  prmgaplcm  16858  prmgapprmo  16860  mreexexd  17454  invfuc  17789  ple1  18245  eqgen  18905  lagsubg  18914  pgpfi  19306  sylow2alem2  19319  sylow2a  19320  sylow3lem4  19331  efgsrel  19435  odadd1  19544  odadd2  19545  gexex  19549  lt6abl  19591  dprd2d2  19742  dmdprdpr  19747  ablfacrp2  19765  ablfac1c  19769  pgpfaclem1  19779  ablfac2  19787  fincygsubgodd  19810  dvdsrmul1  19990  unitmulclb  20002  subrguss  20144  abvres  20205  znfld  20874  znunit  20877  frlmisfrlm  21161  ply1coefsupp  21572  evl1gsumadd  21630  matgsum  21692  pm2mpcl  22052  psmetxrge0  23572  isxmet2d  23586  mettri  23611  xmettri3  23612  mettri3  23613  xmetrtri2  23615  prdsxmetlem  23627  imasdsf1olem  23632  xblss2ps  23660  blss2ps  23662  blss2  23663  blssps  23683  blss  23684  prdsbl  23753  dscmet  23834  nmge0  23879  nmmtri  23884  tngngp3  23926  nlmvscnlem2  23955  nrginvrcnlem  23961  nmoix  23999  nmoleub  24001  blcvx  24067  xrsxmet  24078  opnreen  24100  xrge0tsms  24103  icopnfcnv  24211  xrhmeo  24215  lebnumii  24235  pcophtb  24298  pi1grplem  24318  nmoleub2lem  24383  ipcau2  24504  tcphcphlem1  24505  ipcau  24508  ipcnlem2  24514  rrxcph  24662  minveclem2  24696  minveclem3b  24698  pjthlem1  24707  pjthlem2  24708  ivthlem3  24723  ivth2  24725  ovolfsf  24741  ovolsslem  24754  ovollb2lem  24758  ovollb2  24759  ovolctb  24760  ovolfiniun  24771  ovolicc1  24786  ovolicc2lem4  24790  ovolicc2  24792  nulmbl2  24806  unmbl  24807  ioombl1lem4  24831  uniioombllem4  24856  uniioombllem6  24858  volivth  24877  vitalilem4  24881  itg1ge0  24956  itg1ge0a  24982  itg1lea  24983  itg1climres  24985  mbfi1fseqlem5  24990  itg2ub  25004  itg2seq  25013  itg2uba  25014  itg2splitlem  25019  itg2split  25020  itg2monolem3  25023  itg2mono  25024  itg2i1fseq2  25027  itg2addlem  25029  iblss  25075  itggt0  25114  dvferm2lem  25256  dvlip  25263  dvivthlem1  25278  dvfsumlem2  25297  dvfsumlem3  25298  ftc1lem4  25309  ply1divmo  25406  ply1remlem  25433  fta1glem2  25437  ig1pdvds  25447  plyeq0lem  25477  plydiveu  25564  fta1lem  25573  vieta1lem2  25577  aaliou3lem2  25609  aaliou3lem8  25611  ulmcn  25664  mtest  25669  itgulm  25673  radcnvlem1  25678  radcnvlt1  25683  dvradcnv  25686  pserdvlem2  25693  abelthlem2  25697  abelthlem6  25701  abelthlem7  25703  abelthlem9  25705  tangtx  25768  sinq12gt0  25770  sineq0  25786  cosordlem  25792  tanord  25800  tanregt0  25801  logrnaddcl  25836  logcj  25867  argregt0  25871  argrege0  25872  argimgt0  25873  argimlt0  25874  logimul  25875  logneg2  25876  logdivlti  25881  divlogrlim  25896  logcnlem3  25905  logcnlem4  25906  dvlog2lem  25913  logtayl  25921  rpcxpcl  25937  cxpsqrtlem  25963  cxpaddle  26011  isosctrlem1  26074  asinlem3a  26126  asinlem3  26127  asinneg  26142  asinsinlem  26147  asinsin  26148  atanlogaddlem  26169  atanlogadd  26170  atanlogsublem  26171  atanlogsub  26172  atantan  26179  atanbndlem  26181  atantayl  26193  leibpi  26198  birthdaylem3  26209  areaf  26217  cxploglim  26233  jensenlem2  26243  jensen  26244  logdiflbnd  26250  harmonicbnd4  26266  fsumharmonic  26267  zetacvg  26270  lgamgulmlem2  26285  lgamgulmlem3  26286  lgamcvg2  26310  wilthlem2  26324  wilthimp  26327  ftalem1  26328  ftalem2  26329  ftalem5  26332  basellem6  26341  basellem8  26343  basellem9  26344  chtge0  26367  chtublem  26465  logexprlim  26479  perfectlem1  26483  bcmax  26532  bposlem1  26538  bposlem2  26539  bposlem6  26543  bposlem7  26544  lgsdilem2  26587  lgsqrlem4  26603  lgsquadlem1  26634  2lgsoddprmlem2  26663  2sqlem3  26674  2sqlem8  26680  2sqblem  26685  2sqmod  26690  chebbnd1lem2  26724  chtppilimlem1  26727  chtppilim  26729  chto1ub  26730  vmadivsum  26736  rplogsumlem1  26738  rplogsumlem2  26739  dchrisum0lem1a  26740  rpvmasumlem  26741  dchrisumlem1  26743  dchrisumlem2  26744  dchrvmasumlem2  26752  dchrisum0flblem1  26762  dchrisum0flblem2  26763  dchrisum0lem1b  26769  dchrisum0lem1  26770  dchrisum0lem2a  26771  dchrisum0lem3  26773  dchrisum0  26774  mudivsum  26784  mulogsumlem  26785  mulog2sumlem1  26788  mulog2sumlem2  26789  2vmadivsumlem  26794  chpdifbndlem1  26807  selberg3lem1  26811  selberg4lem1  26814  pntrlog2bndlem1  26831  pntrlog2bndlem2  26832  pntrlog2bndlem3  26833  pntrlog2bndlem4  26834  pntpbnd1a  26839  pntpbnd1  26840  pntpbnd2  26841  pntibndlem2  26845  pntibndlem3  26846  pntlemd  26848  pntlemc  26849  pntlemb  26851  pntlemg  26852  pntlemh  26853  pntlemr  26856  pntlemf  26859  pntlemo  26861  abvcxp  26869  ostth2lem1  26872  padicabv  26884  ostth2lem2  26888  ostth2lem3  26889  ostth2lem4  26890  ostth2  26891  ostth3  26892  nodense  26946  nogt01o  26950  nosupbnd2lem1  26969  noetasuplem3  26989  tgcgr4  27181  legso  27249  krippenlem  27340  midex  27387  oppperpex  27403  ttgcontlem1  27541  axpaschlem  27597  axcontlem8  27628  upgrex  27751  nbfusgrlevtxm1  28033  finsumvtxdgeven  28208  wwlksnextproplem3  28564  clwlkclwwlk2  28655  clwlkclwwlkfolem  28659  clwwlkndivn  28732  ex-ind-dvds  29113  nvabs  29322  nmooge0  29417  nmoolb  29421  siii  29503  minvecolem2  29525  minvecolem4  29530  minvecolem5  29531  hlipgt0  29564  normge0  29776  normpyc  29796  pjhthlem1  30041  pjige0i  30340  nmoplb  30557  nmfnlb  30574  branmfn  30755  pjssdif2i  30824  stlei  30890  xlt2addrd  31368  eliccelico  31385  elicoelioo  31386  bcm1n  31403  dvdszzq  31416  prmdvdsbc  31417  fsumiunle  31430  pfxlsw2ccat  31511  wrdt2ind  31512  xrge0tsmsd  31604  omndmul2  31625  psgnfzto1stlem  31654  cycpmco2lem4  31683  cycpmco2lem5  31684  cyc3conja  31711  archirngz  31730  archiabllem2c  31736  ofldchr  31813  fedgmullem2  32009  extdggt0  32030  madjusmdetlem2  32076  locfinreflem  32088  xrge0iifiso  32183  nexple  32275  gsumesum  32325  esumcst  32329  esumpcvgval  32344  esumcvg  32352  esumiun  32360  measssd  32481  measunl  32482  omssubadd  32567  carsgclctunlem3  32587  pmeasmono  32591  sibfof  32607  oddpwdc  32621  eulerpartlemgc  32629  iwrdsplit  32654  ballotlemsgt1  32777  ballotlemsel1i  32779  sgnmul  32809  signsply0  32830  signstfvc  32853  signsvtp  32862  signsvfpn  32864  fdvposlt  32879  fdvneggt  32880  fdvnegge  32882  logdivsqrle  32930  hgt750lemf  32933  tgoldbachgtde  32940  swrdwlk  33387  subfaclim  33449  erdszelem7  33458  erdszelem8  33459  cvmliftlem2  33547  snmlff  33590  sinccvglem  33929  climlec3  33989  faclim  34002  cofcutr  34188  cofcutrtime  34189  fnejoin1  34653  poimirlem12  35894  poimirlem17  35899  poimirlem19  35901  poimirlem20  35902  poimirlem23  35905  poimirlem28  35910  broucube  35916  mblfinlem2  35920  mblfinlem3  35921  mblfinlem4  35922  ismblfin  35923  itg2addnclem  35933  itg2addnclem3  35935  itg2gt0cn  35937  itggt0cn  35952  ftc1anclem5  35959  ftc1anclem7  35961  ftc1anclem8  35962  isbnd3  36047  ssbnd  36051  heiborlem8  36081  bfplem2  36086  rrncmslem  36095  rrnequiv  36098  rrntotbnd  36099  lcv1  37308  lsatcv0eq  37314  lsatcvat3  37319  cvlsupr2  37610  hlatlej2  37643  cvrval4N  37682  cvratlem  37689  atcvr0eq  37694  2atlt  37707  atbtwnex  37716  athgt  37724  1cvrat  37744  ps-1  37745  hlatexch3N  37748  hlatexch4  37749  3atlem2  37752  atcvrlln2  37787  lplnexllnN  37832  4atlem3a  37865  4atlem10b  37873  4atlem11b  37876  4atlem12b  37879  2lplnja  37887  dalemply  37922  dalemsly  37923  dalem1  37927  dalem6  37936  dalem7  37937  dalem-cly  37939  dalem11  37942  dalem12  37943  dalem16  37947  dalem17  37948  dalem38  37978  dalem44  37984  dalem61  38001  lnatexN  38047  lncvrat  38050  lncmp  38051  paddasslem2  38089  dalawlem3  38141  dalawlem6  38144  dalawlem11  38149  lhpmcvr  38291  lhp2atne  38302  lhp2at0ne  38304  lautj  38361  trlval4  38456  cdlemc2  38460  cdlemc5  38463  cdleme3b  38497  cdleme11c  38529  cdleme19a  38571  cdleme20j  38586  cdleme22f  38614  cdleme23c  38619  cdleme26f2ALTN  38632  cdleme26f2  38633  cdleme35fnpq  38717  cdleme48bw  38770  cdlemg10a  38908  cdlemg11b  38910  cdlemg17g  38935  cdlemg18c  38948  cdlemi1  39086  cdlemk52  39222  dia2dimlem1  39332  dihord1  39486  dihjatcclem4  39689  lcmineqlem15  40305  lcmineqlem19  40309  lcmineqlem22  40312  aks4d1lem1  40324  aks4d1p1p4  40333  aks4d1p1p5  40337  aks4d1p2  40339  aks4d1p3  40340  aks4d1p6  40343  aks4d1p7d1  40344  aks4d1p7  40345  aks4d1p8  40349  aks4d1p9  40350  sticksstones7  40365  metakunt7  40388  metakunt15  40396  metakunt16  40397  2xp3dxp2ge1d  40419  dvdsexpim  40588  dvdsexpnn0  40601  prjspner01  40724  flt4lem5  40749  fltnltalem  40761  fltnlta  40762  3cubeslem1  40768  eldioph2lem1  40844  lzenom  40854  irrapxlem1  40906  irrapxlem4  40909  irrapxlem5  40910  pell14qrgt0  40943  pell1qrge1  40954  pell1qrgap  40958  pellfundge  40966  pellfundex  40970  pellfund14  40982  rmspecsqrtnq  40990  rmxypos  41032  ltrmynn0  41033  ltrmxnn0  41034  jm2.24nn  41044  jm2.17b  41046  jm2.17c  41047  jm2.24  41048  congadd  41051  congsym  41053  congneg  41054  congid  41056  mzpcong  41057  acongrep  41065  acongeq  41068  jm2.18  41073  jm2.19  41078  jm2.23  41081  jm2.25  41084  jm2.26lem3  41086  jm2.15nn0  41088  jm2.16nn0  41089  jm2.27a  41090  jm2.27c  41092  jm3.1lem1  41102  idomrootle  41283  idomsubgmo  41286  sqrtcval  41570  inductionexd  42086  imo72b2  42104  dvgrat  42251  radcnvrat  42253  binomcxplemnn0  42288  binomcxplemnotnn0  42295  cncmpmax  42896  rnmptlb  43116  zltlesub  43159  infxrpnf  43321  xrpnf  43361  fmul01  43457  fmul01lt1lem1  43461  climdivf  43489  sumnnodd  43507  climinf2lem  43583  limsup10exlem  43649  climliminf  43683  dfxlim2v  43724  xlimliminflimsup  43739  dvdivbd  43800  volge0  43838  stoweidlem1  43878  stoweidlem16  43893  stoweidlem18  43895  stoweidlem24  43901  stoweidlem26  43903  stoweidlem36  43913  stoweidlem38  43915  stoweidlem41  43918  stoweidlem42  43919  stoweidlem44  43921  stoweidlem45  43922  stoweidlem48  43925  stoweidlem62  43939  wallispilem5  43946  stirlinglem1  43951  stirlinglem5  43955  stirlinglem7  43957  stirlinglem8  43958  stirlinglem9  43959  stirlinglem11  43961  fourierdlem4  43988  fourierdlem10  43994  fourierdlem37  44021  fourierdlem47  44030  fourierdlem72  44055  fourierdlem74  44057  fourierdlem79  44062  fourierdlem82  44065  fourierdlem89  44072  fourierdlem91  44074  fourierdlem93  44076  fourierdlem103  44086  fourierdlem104  44087  fourierdlem112  44095  etransclem24  44135  etransclem25  44136  etransclem28  44139  etransclem37  44148  etransclem38  44149  etransclem44  44155  meaiuninc3v  44359  vonicclem1  44558  pimconstlt0  44576  smfsuplem1  44686  rlimdmafv  45020  rlimdmafv2  45101  2elfz2melfz  45161  iccpartgtprec  45223  iccpartlt  45227  iccpartgtl  45229  sqrtpwpw2p  45341  fmtnodvds  45347  goldbachthlem1  45348  lighneallem4a  45411  perfectALTVlem1  45524  cznnring  45865  rhmsubcrngc  45938  altgsumbcALT  46040  expnegico01  46210  flnn0div2ge  46230  rege1logbrege0  46255  fllogbd  46257  nnpw2blen  46277  nnolog2flm1  46287  dignn0ldlem  46299  dignn0flhalflem1  46312  dignn0flhalflem2  46313  eenglngeehlnmlem2  46435  itsclc0yqsol  46461  2itscp  46478  itscnhlinecirc02plem1  46479  itscnhlinecirc02plem2  46480  inlinecirc02p  46484