Theorem breqtrrd 5138

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  marypha1lem  9391  marypha2  9397  infsupprpr  9464  unxpwdom  9549  ttrcltr  9676  onadju  10154  nnadju  10158  cfss  10225  tskuni  10743  ltexnq  10935  lt2addmuld  12439  div4p1lem1div2  12444  nn0le2x  12503  mul2lt0rgt0  13063  prodge0ld  13068  ge2halflem1  13075  xrmax1  13142  xrmax2  13143  max1ALT  13153  qbtwnxr  13167  xleadd1a  13220  xlt2add  13227  xlesubadd  13230  xmulgt0  13250  xlemul1a  13255  xov1plusxeqvd  13466  uzsubsubfz  13514  fzctr  13608  subfzo0  13757  flflp1  13776  fldiv4lem1div2uz2  13805  ceilge  13814  modge0  13848  modlt  13849  modid  13865  m1modge3gt1  13890  modaddmodup  13906  sermono  14006  seqf1olem1  14013  seqf1olem2  14014  sqgt0  14098  sqge0  14108  leexp1a  14147  nnlesq  14177  expnbnd  14204  expmulnbnd  14207  discr1  14211  facwordi  14261  faclbnd5  14270  nfile  14331  hashdom  14351  hashgt23el  14396  fi1uzind  14479  brfi1indALT  14482  ccatws1n0  14604  swrds2  14913  cjmulge0  15119  resqrtcl  15226  absge0  15260  sqreulem  15333  amgm2  15343  rlimdm  15524  rlimge0  15554  reccn2  15570  climle  15613  climserle  15636  isercoll2  15642  iseraltlem1  15655  iseralt  15658  isumclim2  15731  isumclim3  15732  isumge0  15739  fsumless  15769  cvgcmp  15789  cvgcmpce  15791  abscvgcvg  15792  isumsup2  15819  isumltss  15821  climcndslem1  15822  climcnds  15824  supcvg  15829  harmonic  15832  expcnv  15837  explecnv  15838  cvgrat  15856  mertenslem1  15857  mertenslem2  15858  clim2div  15862  ntrivcvgtail  15873  iprodclim2  15972  iprodclim3  15973  efcvg  16058  ege2le3  16063  efaddlem  16066  eftlub  16084  effsumlt  16086  tanhlt1  16135  ef01bndlem  16159  sin02gt0  16167  rpnnen2lem4  16192  ruclem2  16207  ruclem3  16208  ruclem9  16213  iddvdsexp  16256  dvdsadd  16279  dvdsfac  16303  dvdsexp2im  16304  dvdsmod  16306  3dvds  16308  omoe  16341  sumeven  16364  divalglem1  16371  flodddiv4t2lthalf  16395  bitsfzo  16412  bitsmod  16413  bitscmp  16415  bitsinv1lem  16418  sadcaddlem  16434  sadadd3  16438  sadaddlem  16443  dvdssqim  16531  dvdsexpim  16532  dvdsmulgcd  16533  nn0seqcvgd  16547  dvdslcm  16575  lcmgcdlem  16583  dvdslcmf  16608  lcmfunsnlem2lem2  16616  mulgcddvds  16632  qredeq  16634  cncongr2  16645  sqnprm  16679  isprm6  16691  dvdszzq  16698  prmdvdsbc  16703  nonsq  16736  hashdvds  16752  prmdiv  16762  odzdvds  16773  pythagtriplem4  16797  pcpre1  16820  pcdvdsb  16847  pcz  16859  pcprmpw2  16860  pcaddlem  16866  pcadd  16867  pcadd2  16868  pcmpt  16870  pcmptdvds  16872  fldivp1  16875  pcfaclem  16876  pockthlem  16883  prmreclem1  16894  prmreclem3  16896  prmreclem5  16898  prmreclem6  16899  4sqlem6  16921  4sqlem8  16923  4sqlem11  16933  4sqlem12  16934  4sqlem14  16936  4sqlem16  16938  vdwlem3  16961  vdwlem9  16967  vdwlem10  16968  vdwlem12  16970  ramub1lem2  17005  prmgap  17037  prmgaplcm  17038  prmgapprmo  17040  mreexexd  17616  invfuc  17946  ple1  18396  eqgen  19120  lagsubg  19134  pgpfi  19542  sylow2alem2  19555  sylow2a  19556  sylow3lem4  19567  efgsrel  19671  odadd1  19785  odadd2  19786  gexex  19790  lt6abl  19832  dprd2d2  19983  dmdprdpr  19988  ablfacrp2  20006  ablfac1c  20010  pgpfaclem1  20020  ablfac2  20028  fincygsubgodd  20051  dvdsrmul1  20285  unitmulclb  20297  subrguss  20503  rhmsubcrngc  20584  abvres  20747  znfld  21477  znunit  21480  frlmisfrlm  21764  ply1coefsupp  22191  evl1gsumadd  22252  matgsum  22331  pm2mpcl  22691  psmetxrge0  24208  isxmet2d  24222  mettri  24247  xmettri3  24248  mettri3  24249  xmetrtri2  24251  prdsxmetlem  24263  imasdsf1olem  24268  xblss2ps  24296  blss2ps  24298  blss2  24299  blssps  24319  blss  24320  prdsbl  24386  dscmet  24467  nmge0  24512  nmmtri  24517  tngngp3  24551  nlmvscnlem2  24580  nrginvrcnlem  24586  nmoix  24624  nmoleub  24626  blcvx  24693  xrsxmet  24705  opnreen  24727  xrge0tsms  24730  icopnfcnv  24847  xrhmeo  24851  lebnumii  24872  pcophtb  24936  pi1grplem  24956  nmoleub2lem  25021  ipcau2  25141  tcphcphlem1  25142  ipcau  25145  ipcnlem2  25151  rrxcph  25299  minveclem2  25333  minveclem3b  25335  pjthlem1  25344  pjthlem2  25345  ivthlem3  25361  ivth2  25363  ovolfsf  25379  ovolsslem  25392  ovollb2lem  25396  ovollb2  25397  ovolctb  25398  ovolfiniun  25409  ovolicc1  25424  ovolicc2lem4  25428  ovolicc2  25430  nulmbl2  25444  unmbl  25445  ioombl1lem4  25469  uniioombllem4  25494  uniioombllem6  25496  volivth  25515  vitalilem4  25519  itg1ge0  25594  itg1ge0a  25619  itg1lea  25620  itg1climres  25622  mbfi1fseqlem5  25627  itg2ub  25641  itg2seq  25650  itg2uba  25651  itg2splitlem  25656  itg2split  25657  itg2monolem3  25660  itg2mono  25661  itg2i1fseq2  25664  itg2addlem  25666  iblss  25713  itggt0  25752  dvferm2lem  25897  dvlip  25905  dvivthlem1  25920  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  ftc1lem4  25953  ply1divmo  26048  ply1remlem  26077  fta1glem2  26081  idomrootle  26085  ig1pdvds  26092  plyeq0lem  26122  plydiveu  26213  fta1lem  26222  vieta1lem2  26226  aaliou3lem2  26258  aaliou3lem8  26260  ulmcn  26315  mtest  26320  itgulm  26324  radcnvlem1  26329  radcnvlt1  26334  dvradcnv  26337  pserdvlem2  26345  abelthlem2  26349  abelthlem6  26353  abelthlem7  26355  abelthlem9  26357  tangtx  26421  sinq12gt0  26423  sineq0  26440  cosordlem  26446  tanord  26454  tanregt0  26455  logrnaddcl  26490  logcj  26522  argregt0  26526  argrege0  26527  argimgt0  26528  argimlt0  26529  logimul  26530  logneg2  26531  logdivlti  26536  divlogrlim  26551  logcnlem3  26560  logcnlem4  26561  dvlog2lem  26568  logtayl  26576  rpcxpcl  26592  cxpsqrtlem  26618  cxpaddle  26669  isosctrlem1  26735  asinlem3a  26787  asinlem3  26788  asinneg  26803  asinsinlem  26808  asinsin  26809  atanlogaddlem  26830  atanlogadd  26831  atanlogsublem  26832  atanlogsub  26833  atantan  26840  atanbndlem  26842  atantayl  26854  leibpi  26859  birthdaylem3  26870  areaf  26878  cxploglim  26895  jensenlem2  26905  jensen  26906  logdiflbnd  26912  harmonicbnd4  26928  fsumharmonic  26929  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamcvg2  26972  wilthlem2  26986  wilthimp  26989  ftalem1  26990  ftalem2  26991  ftalem5  26994  basellem6  27003  basellem8  27005  basellem9  27006  chtge0  27029  chtublem  27129  logexprlim  27143  perfectlem1  27147  bcmax  27196  bposlem1  27202  bposlem2  27203  bposlem6  27207  bposlem7  27208  lgsdilem2  27251  lgsqrlem4  27267  lgsquadlem1  27298  2lgsoddprmlem2  27327  2sqlem3  27338  2sqlem8  27344  2sqblem  27349  2sqmod  27354  chebbnd1lem2  27388  chtppilimlem1  27391  chtppilim  27393  chto1ub  27394  vmadivsum  27400  rplogsumlem1  27402  rplogsumlem2  27403  dchrisum0lem1a  27404  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrvmasumlem2  27416  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem3  27437  dchrisum0  27438  mudivsum  27448  mulogsumlem  27449  mulog2sumlem1  27452  mulog2sumlem2  27453  2vmadivsumlem  27458  chpdifbndlem1  27471  selberg3lem1  27475  selberg4lem1  27478  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntibndlem2  27509  pntibndlem3  27510  pntlemd  27512  pntlemc  27513  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemr  27520  pntlemf  27523  pntlemo  27525  abvcxp  27533  ostth2lem1  27536  padicabv  27548  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth2  27555  ostth3  27556  nodense  27611  nogt01o  27615  nosupbnd2lem1  27634  noetasuplem3  27654  maxs1  27684  maxs2  27685  cofcutr  27839  cofcutrtime  27842  addsuniflem  27915  negsunif  27968  ssltmul2  28058  precsexlem11  28126  abssge0  28154  sleabs  28157  onscutlt  28172  om2noseqlt  28200  expsgt0  28329  halfcut  28340  addhalfcut  28341  tgcgr4  28465  legso  28533  krippenlem  28624  midex  28671  oppperpex  28687  ttgcontlem1  28819  axpaschlem  28874  axcontlem8  28905  upgrex  29026  nbfusgrlevtxm1  29311  finsumvtxdgeven  29487  wwlksnextproplem3  29848  clwlkclwwlk2  29939  clwlkclwwlkfolem  29943  clwwlkndivn  30016  ex-ind-dvds  30397  nvabs  30608  nmooge0  30703  nmoolb  30707  siii  30789  minvecolem2  30811  minvecolem4  30816  minvecolem5  30817  hlipgt0  30850  normge0  31062  normpyc  31082  pjhthlem1  31327  pjige0i  31626  nmoplb  31843  nmfnlb  31860  branmfn  32041  pjssdif2i  32110  stlei  32176  xlt2addrd  32689  eliccelico  32707  elicoelioo  32708  bcm1n  32725  fsumiunle  32761  sgnmul  32767  nexple  32776  expevenpos  32778  ccatdmss  32878  pfxlsw2ccat  32879  wrdt2ind  32882  chnub  32945  xrge0tsmsd  33009  gsumwrd2dccatlem  33013  omndmul2  33033  psgnfzto1stlem  33064  cycpmco2lem4  33093  cycpmco2lem5  33094  cyc3conja  33121  archirngz  33150  archiabllem2c  33156  ofldchr  33299  rprmasso2  33504  rprmirred  33509  1arithufdlem3  33524  lbslelsp  33600  fedgmullem2  33633  extdggt0  33660  evls1fldgencl  33672  fldextrspunlem1  33677  algextdeglem8  33721  rtelextdg2lem  33723  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  madjusmdetlem2  33825  locfinreflem  33837  xrge0iifiso  33932  gsumesum  34056  esumcst  34060  esumpcvgval  34075  esumcvg  34083  esumiun  34091  measssd  34212  measunl  34213  omssubadd  34298  carsgclctunlem3  34318  pmeasmono  34322  sibfof  34338  oddpwdc  34352  eulerpartlemgc  34360  iwrdsplit  34385  ballotlemsgt1  34509  ballotlemsel1i  34511  signsply0  34549  signstfvc  34572  signsvtp  34581  signsvfpn  34583  fdvposlt  34597  fdvneggt  34598  fdvnegge  34600  logdivsqrle  34648  hgt750lemf  34651  tgoldbachgtde  34658  swrdwlk  35121  subfaclim  35182  erdszelem7  35191  erdszelem8  35192  cvmliftlem2  35280  snmlff  35323  sinccvglem  35666  climlec3  35728  faclim  35740  fnejoin1  36363  poimirlem12  37633  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem28  37649  broucube  37655  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnclem3  37674  itg2gt0cn  37676  itggt0cn  37691  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  isbnd3  37785  ssbnd  37789  heiborlem8  37819  bfplem2  37824  rrncmslem  37833  rrnequiv  37836  rrntotbnd  37837  lcv1  39041  lsatcv0eq  39047  lsatcvat3  39052  cvlsupr2  39343  hlatlej2  39376  cvrval4N  39415  cvratlem  39422  atcvr0eq  39427  2atlt  39440  atbtwnex  39449  athgt  39457  1cvrat  39477  ps-1  39478  hlatexch3N  39481  hlatexch4  39482  3atlem2  39485  atcvrlln2  39520  lplnexllnN  39565  4atlem3a  39598  4atlem10b  39606  4atlem11b  39609  4atlem12b  39612  2lplnja  39620  dalemply  39655  dalemsly  39656  dalem1  39660  dalem6  39669  dalem7  39670  dalem-cly  39672  dalem11  39675  dalem12  39676  dalem16  39680  dalem17  39681  dalem38  39711  dalem44  39717  dalem61  39734  lnatexN  39780  lncvrat  39783  lncmp  39784  paddasslem2  39822  dalawlem3  39874  dalawlem6  39877  dalawlem11  39882  lhpmcvr  40024  lhp2atne  40035  lhp2at0ne  40037  lautj  40094  trlval4  40189  cdlemc2  40193  cdlemc5  40196  cdleme3b  40230  cdleme11c  40262  cdleme19a  40304  cdleme20j  40319  cdleme22f  40347  cdleme23c  40352  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme35fnpq  40450  cdleme48bw  40503  cdlemg10a  40641  cdlemg11b  40643  cdlemg17g  40668  cdlemg18c  40681  cdlemi1  40819  cdlemk52  40955  dia2dimlem1  41065  dihord1  41219  dihjatcclem4  41422  lcmineqlem15  42038  lcmineqlem19  42042  lcmineqlem22  42045  aks4d1lem1  42057  aks4d1p1p4  42066  aks4d1p1p5  42070  aks4d1p2  42072  aks4d1p3  42073  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  aks6d1c1p6  42109  aks6d1c1  42111  aks6d1c2  42125  sticksstones7  42147  aks6d1c7lem1  42175  unitscyglem4  42193  dvdsexpnn0  42329  prjspner01  42620  flt4lem5  42645  fltnltalem  42657  fltnlta  42658  3cubeslem1  42679  eldioph2lem1  42755  lzenom  42765  irrapxlem1  42817  irrapxlem4  42820  irrapxlem5  42821  pell14qrgt0  42854  pell1qrge1  42865  pell1qrgap  42869  pellfundge  42877  pellfundex  42881  pellfund14  42893  rmspecsqrtnq  42901  rmxypos  42943  ltrmynn0  42944  ltrmxnn0  42945  jm2.24nn  42955  jm2.17b  42957  jm2.17c  42958  jm2.24  42959  congadd  42962  congsym  42964  congneg  42965  congid  42967  mzpcong  42968  acongrep  42976  acongeq  42979  jm2.18  42984  jm2.19  42989  jm2.23  42992  jm2.25  42995  jm2.26lem3  42997  jm2.15nn0  42999  jm2.16nn0  43000  jm2.27a  43001  jm2.27c  43003  jm3.1lem1  43013  idomsubgmo  43189  sqrtcval  43637  inductionexd  44151  imo72b2lem0  44161  imo72b2  44168  dvgrat  44308  radcnvrat  44310  binomcxplemnn0  44345  binomcxplemnotnn0  44352  cncmpmax  45033  rnmptlb  45244  zltlesub  45290  infxrpnf  45449  xrpnf  45488  fmul01  45585  fmul01lt1lem1  45589  climdivf  45617  sumnnodd  45635  climinf2lem  45711  limsup10exlem  45777  climliminf  45811  dfxlim2v  45852  xlimliminflimsup  45867  dvdivbd  45928  volge0  45966  stoweidlem1  46006  stoweidlem16  46021  stoweidlem18  46023  stoweidlem24  46029  stoweidlem26  46031  stoweidlem36  46041  stoweidlem38  46043  stoweidlem41  46046  stoweidlem42  46047  stoweidlem44  46049  stoweidlem45  46050  stoweidlem48  46053  stoweidlem62  46067  wallispilem5  46074  stirlinglem1  46079  stirlinglem5  46083  stirlinglem7  46085  stirlinglem8  46086  stirlinglem9  46087  stirlinglem11  46089  fourierdlem4  46116  fourierdlem10  46122  fourierdlem37  46149  fourierdlem47  46158  fourierdlem72  46183  fourierdlem74  46185  fourierdlem79  46190  fourierdlem82  46193  fourierdlem89  46200  fourierdlem91  46202  fourierdlem93  46204  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  etransclem24  46263  etransclem25  46264  etransclem28  46267  etransclem37  46276  etransclem38  46277  etransclem44  46283  meaiuninc3v  46489  vonicclem1  46688  pimconstlt0  46706  smfsuplem1  46816  rlimdmafv  47182  rlimdmafv2  47263  2elfz2melfz  47323  iccpartgtprec  47425  iccpartlt  47429  iccpartgtl  47431  sqrtpwpw2p  47543  fmtnodvds  47549  goldbachthlem1  47550  lighneallem4a  47613  perfectALTVlem1  47726  uhgrimgrlim  47990  cznnring  48254  altgsumbcALT  48345  expnegico01  48511  flnn0div2ge  48526  rege1logbrege0  48551  fllogbd  48553  nnpw2blen  48573  nnolog2flm1  48583  dignn0ldlem  48595  dignn0flhalflem1  48608  dignn0flhalflem2  48609  eenglngeehlnmlem2  48731  itsclc0yqsol  48757  2itscp  48774  itscnhlinecirc02plem1  48775  itscnhlinecirc02plem2  48776  inlinecirc02p  48780