Theorem breqtrrd 5130

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  marypha1lem  9360  marypha2  9366  infsupprpr  9433  unxpwdom  9518  ttrcltr  9645  onadju  10123  nnadju  10127  cfss  10194  tskuni  10712  ltexnq  10904  lt2addmuld  12408  div4p1lem1div2  12413  nn0le2x  12472  mul2lt0rgt0  13032  prodge0ld  13037  ge2halflem1  13044  xrmax1  13111  xrmax2  13112  max1ALT  13122  qbtwnxr  13136  xleadd1a  13189  xlt2add  13196  xlesubadd  13199  xmulgt0  13219  xlemul1a  13224  xov1plusxeqvd  13435  uzsubsubfz  13483  fzctr  13577  subfzo0  13726  flflp1  13745  fldiv4lem1div2uz2  13774  ceilge  13783  modge0  13817  modlt  13818  modid  13834  m1modge3gt1  13859  modaddmodup  13875  sermono  13975  seqf1olem1  13982  seqf1olem2  13983  sqgt0  14067  sqge0  14077  leexp1a  14116  nnlesq  14146  expnbnd  14173  expmulnbnd  14176  discr1  14180  facwordi  14230  faclbnd5  14239  nfile  14300  hashdom  14320  hashgt23el  14365  fi1uzind  14448  brfi1indALT  14451  ccatws1n0  14573  swrds2  14882  cjmulge0  15088  resqrtcl  15195  absge0  15229  sqreulem  15302  amgm2  15312  rlimdm  15493  rlimge0  15523  reccn2  15539  climle  15582  climserle  15605  isercoll2  15611  iseraltlem1  15624  iseralt  15627  isumclim2  15700  isumclim3  15701  isumge0  15708  fsumless  15738  cvgcmp  15758  cvgcmpce  15760  abscvgcvg  15761  isumsup2  15788  isumltss  15790  climcndslem1  15791  climcnds  15793  supcvg  15798  harmonic  15801  expcnv  15806  explecnv  15807  cvgrat  15825  mertenslem1  15826  mertenslem2  15827  clim2div  15831  ntrivcvgtail  15842  iprodclim2  15941  iprodclim3  15942  efcvg  16027  ege2le3  16032  efaddlem  16035  eftlub  16053  effsumlt  16055  tanhlt1  16104  ef01bndlem  16128  sin02gt0  16136  rpnnen2lem4  16161  ruclem2  16176  ruclem3  16177  ruclem9  16182  iddvdsexp  16225  dvdsadd  16248  dvdsfac  16272  dvdsexp2im  16273  dvdsmod  16275  3dvds  16277  omoe  16310  sumeven  16333  divalglem1  16340  flodddiv4t2lthalf  16364  bitsfzo  16381  bitsmod  16382  bitscmp  16384  bitsinv1lem  16387  sadcaddlem  16403  sadadd3  16407  sadaddlem  16412  dvdssqim  16500  dvdsexpim  16501  dvdsmulgcd  16502  nn0seqcvgd  16516  dvdslcm  16544  lcmgcdlem  16552  dvdslcmf  16577  lcmfunsnlem2lem2  16585  mulgcddvds  16601  qredeq  16603  cncongr2  16614  sqnprm  16648  isprm6  16660  dvdszzq  16667  prmdvdsbc  16672  nonsq  16705  hashdvds  16721  prmdiv  16731  odzdvds  16742  pythagtriplem4  16766  pcpre1  16789  pcdvdsb  16816  pcz  16828  pcprmpw2  16829  pcaddlem  16835  pcadd  16836  pcadd2  16837  pcmpt  16839  pcmptdvds  16841  fldivp1  16844  pcfaclem  16845  pockthlem  16852  prmreclem1  16863  prmreclem3  16865  prmreclem5  16867  prmreclem6  16868  4sqlem6  16890  4sqlem8  16892  4sqlem11  16902  4sqlem12  16903  4sqlem14  16905  4sqlem16  16907  vdwlem3  16930  vdwlem9  16936  vdwlem10  16937  vdwlem12  16939  ramub1lem2  16974  prmgap  17006  prmgaplcm  17007  prmgapprmo  17009  mreexexd  17589  invfuc  17919  ple1  18369  eqgen  19095  lagsubg  19109  pgpfi  19519  sylow2alem2  19532  sylow2a  19533  sylow3lem4  19544  efgsrel  19648  odadd1  19762  odadd2  19763  gexex  19767  lt6abl  19809  dprd2d2  19960  dmdprdpr  19965  ablfacrp2  19983  ablfac1c  19987  pgpfaclem1  19997  ablfac2  20005  fincygsubgodd  20028  omndmul2  20047  dvdsrmul1  20289  unitmulclb  20301  subrguss  20507  rhmsubcrngc  20588  abvres  20751  znfld  21502  znunit  21505  ofldchr  21518  frlmisfrlm  21790  ply1coefsupp  22217  evl1gsumadd  22278  matgsum  22357  pm2mpcl  22717  psmetxrge0  24234  isxmet2d  24248  mettri  24273  xmettri3  24274  mettri3  24275  xmetrtri2  24277  prdsxmetlem  24289  imasdsf1olem  24294  xblss2ps  24322  blss2ps  24324  blss2  24325  blssps  24345  blss  24346  prdsbl  24412  dscmet  24493  nmge0  24538  nmmtri  24543  tngngp3  24577  nlmvscnlem2  24606  nrginvrcnlem  24612  nmoix  24650  nmoleub  24652  blcvx  24719  xrsxmet  24731  opnreen  24753  xrge0tsms  24756  icopnfcnv  24873  xrhmeo  24877  lebnumii  24898  pcophtb  24962  pi1grplem  24982  nmoleub2lem  25047  ipcau2  25167  tcphcphlem1  25168  ipcau  25171  ipcnlem2  25177  rrxcph  25325  minveclem2  25359  minveclem3b  25361  pjthlem1  25370  pjthlem2  25371  ivthlem3  25387  ivth2  25389  ovolfsf  25405  ovolsslem  25418  ovollb2lem  25422  ovollb2  25423  ovolctb  25424  ovolfiniun  25435  ovolicc1  25450  ovolicc2lem4  25454  ovolicc2  25456  nulmbl2  25470  unmbl  25471  ioombl1lem4  25495  uniioombllem4  25520  uniioombllem6  25522  volivth  25541  vitalilem4  25545  itg1ge0  25620  itg1ge0a  25645  itg1lea  25646  itg1climres  25648  mbfi1fseqlem5  25653  itg2ub  25667  itg2seq  25676  itg2uba  25677  itg2splitlem  25682  itg2split  25683  itg2monolem3  25686  itg2mono  25687  itg2i1fseq2  25690  itg2addlem  25692  iblss  25739  itggt0  25778  dvferm2lem  25923  dvlip  25931  dvivthlem1  25946  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  ftc1lem4  25979  ply1divmo  26074  ply1remlem  26103  fta1glem2  26107  idomrootle  26111  ig1pdvds  26118  plyeq0lem  26148  plydiveu  26239  fta1lem  26248  vieta1lem2  26252  aaliou3lem2  26284  aaliou3lem8  26286  ulmcn  26341  mtest  26346  itgulm  26350  radcnvlem1  26355  radcnvlt1  26360  dvradcnv  26363  pserdvlem2  26371  abelthlem2  26375  abelthlem6  26379  abelthlem7  26381  abelthlem9  26383  tangtx  26447  sinq12gt0  26449  sineq0  26466  cosordlem  26472  tanord  26480  tanregt0  26481  logrnaddcl  26516  logcj  26548  argregt0  26552  argrege0  26553  argimgt0  26554  argimlt0  26555  logimul  26556  logneg2  26557  logdivlti  26562  divlogrlim  26577  logcnlem3  26586  logcnlem4  26587  dvlog2lem  26594  logtayl  26602  rpcxpcl  26618  cxpsqrtlem  26644  cxpaddle  26695  isosctrlem1  26761  asinlem3a  26813  asinlem3  26814  asinneg  26829  asinsinlem  26834  asinsin  26835  atanlogaddlem  26856  atanlogadd  26857  atanlogsublem  26858  atanlogsub  26859  atantan  26866  atanbndlem  26868  atantayl  26880  leibpi  26885  birthdaylem3  26896  areaf  26904  cxploglim  26921  jensenlem2  26931  jensen  26932  logdiflbnd  26938  harmonicbnd4  26954  fsumharmonic  26955  zetacvg  26958  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamcvg2  26998  wilthlem2  27012  wilthimp  27015  ftalem1  27016  ftalem2  27017  ftalem5  27020  basellem6  27029  basellem8  27031  basellem9  27032  chtge0  27055  chtublem  27155  logexprlim  27169  perfectlem1  27173  bcmax  27222  bposlem1  27228  bposlem2  27229  bposlem6  27233  bposlem7  27234  lgsdilem2  27277  lgsqrlem4  27293  lgsquadlem1  27324  2lgsoddprmlem2  27353  2sqlem3  27364  2sqlem8  27370  2sqblem  27375  2sqmod  27380  chebbnd1lem2  27414  chtppilimlem1  27417  chtppilim  27419  chto1ub  27420  vmadivsum  27426  rplogsumlem1  27428  rplogsumlem2  27429  dchrisum0lem1a  27430  rpvmasumlem  27431  dchrisumlem1  27433  dchrisumlem2  27434  dchrvmasumlem2  27442  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem3  27463  dchrisum0  27464  mudivsum  27474  mulogsumlem  27475  mulog2sumlem1  27478  mulog2sumlem2  27479  2vmadivsumlem  27484  chpdifbndlem1  27497  selberg3lem1  27501  selberg4lem1  27504  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem2  27535  pntibndlem3  27536  pntlemd  27538  pntlemc  27539  pntlemb  27541  pntlemg  27542  pntlemh  27543  pntlemr  27546  pntlemf  27549  pntlemo  27551  abvcxp  27559  ostth2lem1  27562  padicabv  27574  ostth2lem2  27578  ostth2lem3  27579  ostth2lem4  27580  ostth2  27581  ostth3  27582  nodense  27637  nogt01o  27641  nosupbnd2lem1  27660  noetasuplem3  27680  maxs1  27710  maxs2  27711  eqscut3  27770  cofcutr  27872  cofcutrtime  27875  addsuniflem  27948  negsunif  28001  ssltmul2  28091  precsexlem11  28159  abssge0  28187  sleabs  28190  onscutlt  28205  om2noseqlt  28233  zsoring  28336  expsgt0  28364  halfcut  28381  addhalfcut  28382  tgcgr4  28511  legso  28579  krippenlem  28670  midex  28717  oppperpex  28733  ttgcontlem1  28865  axpaschlem  28920  axcontlem8  28951  upgrex  29072  nbfusgrlevtxm1  29357  finsumvtxdgeven  29533  wwlksnextproplem3  29891  clwlkclwwlk2  29982  clwlkclwwlkfolem  29986  clwwlkndivn  30059  ex-ind-dvds  30440  nvabs  30651  nmooge0  30746  nmoolb  30750  siii  30832  minvecolem2  30854  minvecolem4  30859  minvecolem5  30860  hlipgt0  30893  normge0  31105  normpyc  31125  pjhthlem1  31370  pjige0i  31669  nmoplb  31886  nmfnlb  31903  branmfn  32084  pjssdif2i  32153  stlei  32219  xlt2addrd  32732  eliccelico  32750  elicoelioo  32751  bcm1n  32768  fsumiunle  32804  sgnmul  32810  nexple  32819  expevenpos  32821  ccatdmss  32921  pfxlsw2ccat  32922  wrdt2ind  32925  chnub  32984  xrge0tsmsd  33045  gsumwrd2dccatlem  33049  psgnfzto1stlem  33072  cycpmco2lem4  33101  cycpmco2lem5  33102  cyc3conja  33129  archirngz  33158  archiabllem2c  33164  rprmasso2  33490  rprmirred  33495  1arithufdlem3  33510  lbslelsp  33586  fedgmullem2  33619  extdggt0  33646  evls1fldgencl  33658  fldextrspunlem1  33663  algextdeglem8  33707  rtelextdg2lem  33709  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  madjusmdetlem2  33811  locfinreflem  33823  xrge0iifiso  33918  gsumesum  34042  esumcst  34046  esumpcvgval  34061  esumcvg  34069  esumiun  34077  measssd  34198  measunl  34199  omssubadd  34284  carsgclctunlem3  34304  pmeasmono  34308  sibfof  34324  oddpwdc  34338  eulerpartlemgc  34346  iwrdsplit  34371  ballotlemsgt1  34495  ballotlemsel1i  34497  signsply0  34535  signstfvc  34558  signsvtp  34567  signsvfpn  34569  fdvposlt  34583  fdvneggt  34584  fdvnegge  34586  logdivsqrle  34634  hgt750lemf  34637  tgoldbachgtde  34644  swrdwlk  35107  subfaclim  35168  erdszelem7  35177  erdszelem8  35178  cvmliftlem2  35266  snmlff  35309  sinccvglem  35652  climlec3  35714  faclim  35726  fnejoin1  36349  poimirlem12  37619  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem28  37635  broucube  37641  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  itg2addnclem  37658  itg2addnclem3  37660  itg2gt0cn  37662  itggt0cn  37677  ftc1anclem5  37684  ftc1anclem7  37686  ftc1anclem8  37687  isbnd3  37771  ssbnd  37775  heiborlem8  37805  bfplem2  37810  rrncmslem  37819  rrnequiv  37822  rrntotbnd  37823  lcv1  39027  lsatcv0eq  39033  lsatcvat3  39038  cvlsupr2  39329  hlatlej2  39362  cvrval4N  39401  cvratlem  39408  atcvr0eq  39413  2atlt  39426  atbtwnex  39435  athgt  39443  1cvrat  39463  ps-1  39464  hlatexch3N  39467  hlatexch4  39468  3atlem2  39471  atcvrlln2  39506  lplnexllnN  39551  4atlem3a  39584  4atlem10b  39592  4atlem11b  39595  4atlem12b  39598  2lplnja  39606  dalemply  39641  dalemsly  39642  dalem1  39646  dalem6  39655  dalem7  39656  dalem-cly  39658  dalem11  39661  dalem12  39662  dalem16  39666  dalem17  39667  dalem38  39697  dalem44  39703  dalem61  39720  lnatexN  39766  lncvrat  39769  lncmp  39770  paddasslem2  39808  dalawlem3  39860  dalawlem6  39863  dalawlem11  39868  lhpmcvr  40010  lhp2atne  40021  lhp2at0ne  40023  lautj  40080  trlval4  40175  cdlemc2  40179  cdlemc5  40182  cdleme3b  40216  cdleme11c  40248  cdleme19a  40290  cdleme20j  40305  cdleme22f  40333  cdleme23c  40338  cdleme26f2ALTN  40351  cdleme26f2  40352  cdleme35fnpq  40436  cdleme48bw  40489  cdlemg10a  40627  cdlemg11b  40629  cdlemg17g  40654  cdlemg18c  40667  cdlemi1  40805  cdlemk52  40941  dia2dimlem1  41051  dihord1  41205  dihjatcclem4  41408  lcmineqlem15  42024  lcmineqlem19  42028  lcmineqlem22  42031  aks4d1lem1  42043  aks4d1p1p4  42052  aks4d1p1p5  42056  aks4d1p2  42058  aks4d1p3  42059  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  aks6d1c1p6  42095  aks6d1c1  42097  aks6d1c2  42111  sticksstones7  42133  aks6d1c7lem1  42161  unitscyglem4  42179  dvdsexpnn0  42315  prjspner01  42606  flt4lem5  42631  fltnltalem  42643  fltnlta  42644  3cubeslem1  42665  eldioph2lem1  42741  lzenom  42751  irrapxlem1  42803  irrapxlem4  42806  irrapxlem5  42807  pell14qrgt0  42840  pell1qrge1  42851  pell1qrgap  42855  pellfundge  42863  pellfundex  42867  pellfund14  42879  rmspecsqrtnq  42887  rmxypos  42929  ltrmynn0  42930  ltrmxnn0  42931  jm2.24nn  42941  jm2.17b  42943  jm2.17c  42944  jm2.24  42945  congadd  42948  congsym  42950  congneg  42951  congid  42953  mzpcong  42954  acongrep  42962  acongeq  42965  jm2.18  42970  jm2.19  42975  jm2.23  42978  jm2.25  42981  jm2.26lem3  42983  jm2.15nn0  42985  jm2.16nn0  42986  jm2.27a  42987  jm2.27c  42989  jm3.1lem1  42999  idomsubgmo  43175  sqrtcval  43623  inductionexd  44137  imo72b2lem0  44147  imo72b2  44154  dvgrat  44294  radcnvrat  44296  binomcxplemnn0  44331  binomcxplemnotnn0  44338  cncmpmax  45019  rnmptlb  45230  zltlesub  45276  infxrpnf  45435  xrpnf  45474  fmul01  45571  fmul01lt1lem1  45575  climdivf  45603  sumnnodd  45621  climinf2lem  45697  limsup10exlem  45763  climliminf  45797  dfxlim2v  45838  xlimliminflimsup  45853  dvdivbd  45914  volge0  45952  stoweidlem1  45992  stoweidlem16  46007  stoweidlem18  46009  stoweidlem24  46015  stoweidlem26  46017  stoweidlem36  46027  stoweidlem38  46029  stoweidlem41  46032  stoweidlem42  46033  stoweidlem44  46035  stoweidlem45  46036  stoweidlem48  46039  stoweidlem62  46053  wallispilem5  46060  stirlinglem1  46065  stirlinglem5  46069  stirlinglem7  46071  stirlinglem8  46072  stirlinglem9  46073  stirlinglem11  46075  fourierdlem4  46102  fourierdlem10  46108  fourierdlem37  46135  fourierdlem47  46144  fourierdlem72  46169  fourierdlem74  46171  fourierdlem79  46176  fourierdlem82  46179  fourierdlem89  46186  fourierdlem91  46188  fourierdlem93  46190  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  etransclem24  46249  etransclem25  46250  etransclem28  46253  etransclem37  46262  etransclem38  46263  etransclem44  46269  meaiuninc3v  46475  vonicclem1  46674  pimconstlt0  46692  smfsuplem1  46802  rlimdmafv  47171  rlimdmafv2  47252  2elfz2melfz  47312  iccpartgtprec  47414  iccpartlt  47418  iccpartgtl  47420  sqrtpwpw2p  47532  fmtnodvds  47538  goldbachthlem1  47539  lighneallem4a  47602  perfectALTVlem1  47715  uhgrimgrlim  47979  cznnring  48243  altgsumbcALT  48334  expnegico01  48500  flnn0div2ge  48515  rege1logbrege0  48540  fllogbd  48542  nnpw2blen  48562  nnolog2flm1  48572  dignn0ldlem  48584  dignn0flhalflem1  48597  dignn0flhalflem2  48598  eenglngeehlnmlem2  48720  itsclc0yqsol  48746  2itscp  48763  itscnhlinecirc02plem1  48764  itscnhlinecirc02plem2  48765  inlinecirc02p  48769