Theorem breqtrrd 5081

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

Syntax hints:   → wi 4   = wceq 1543   class class class wbr 5053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054

This theorem is referenced by:  marypha1lem  9049  marypha2  9055  infsupprpr  9120  unxpwdom  9205  onadju  9807  nnadju  9811  cfss  9879  tskuni  10397  ltexnq  10589  lt2addmuld  12080  div4p1lem1div2  12085  mul2lt0rgt0  12689  prodge0ld  12694  xrmax1  12765  xrmax2  12766  max1ALT  12776  qbtwnxr  12790  xleadd1a  12843  xlt2add  12850  xlesubadd  12853  xmulgt0  12873  xlemul1a  12878  xov1plusxeqvd  13086  uzsubsubfz  13134  fzctr  13224  subfzo0  13364  flflp1  13382  fldiv4lem1div2uz2  13411  ceilge  13419  modge0  13452  modlt  13453  modid  13469  m1modge3gt1  13491  modaddmodup  13507  sermono  13608  seqf1olem1  13615  seqf1olem2  13616  sqgt0  13697  sqge0  13707  leexp1a  13745  nnlesq  13774  expnbnd  13799  expmulnbnd  13802  discr1  13806  facwordi  13855  faclbnd5  13864  nfile  13926  hashdom  13946  hashgt23el  13991  fi1uzind  14063  brfi1indALT  14066  ccatws1n0  14194  swrds2  14505  cjmulge0  14709  resqrtcl  14817  absge0  14851  sqreulem  14923  amgm2  14933  rlimdm  15112  rlimge0  15142  reccn2  15158  climle  15201  climserle  15226  isercoll2  15232  iseraltlem1  15245  iseralt  15248  isumclim2  15322  isumclim3  15323  isumge0  15330  fsumless  15360  cvgcmp  15380  cvgcmpce  15382  abscvgcvg  15383  isumsup2  15410  isumltss  15412  climcndslem1  15413  climcnds  15415  supcvg  15420  harmonic  15423  expcnv  15428  explecnv  15429  cvgrat  15447  mertenslem1  15448  mertenslem2  15449  clim2div  15453  ntrivcvgtail  15464  iprodclim2  15561  iprodclim3  15562  efcvg  15646  ege2le3  15651  efaddlem  15654  eftlub  15670  effsumlt  15672  tanhlt1  15721  ef01bndlem  15745  sin02gt0  15753  rpnnen2lem4  15778  ruclem2  15793  ruclem3  15794  ruclem9  15799  iddvdsexp  15841  dvdsadd  15863  dvdsfac  15887  dvdsexp2im  15888  dvdsmod  15890  3dvds  15892  omoe  15925  sumeven  15948  divalglem1  15955  flodddiv4t2lthalf  15977  bitsfzo  15994  bitsmod  15995  bitscmp  15997  bitsinv1lem  16000  sadcaddlem  16016  sadadd3  16020  sadaddlem  16025  dvdssqim  16116  dvdsmulgcd  16117  nn0seqcvgd  16127  dvdslcm  16155  lcmgcdlem  16163  dvdslcmf  16188  lcmfunsnlem2lem2  16196  mulgcddvds  16212  qredeq  16214  cncongr2  16225  sqnprm  16259  isprm6  16271  nonsq  16315  hashdvds  16328  prmdiv  16338  odzdvds  16348  pythagtriplem4  16372  pcpre1  16395  pcdvdsb  16422  pcz  16434  pcprmpw2  16435  pcaddlem  16441  pcadd  16442  pcadd2  16443  pcmpt  16445  pcmptdvds  16447  fldivp1  16450  pcfaclem  16451  pockthlem  16458  prmreclem1  16469  prmreclem3  16471  prmreclem5  16473  prmreclem6  16474  4sqlem6  16496  4sqlem8  16498  4sqlem11  16508  4sqlem12  16509  4sqlem14  16511  4sqlem16  16513  vdwlem3  16536  vdwlem9  16542  vdwlem10  16543  vdwlem12  16545  ramub1lem2  16580  prmgap  16612  prmgaplcm  16613  prmgapprmo  16615  mreexexd  17151  invfuc  17483  ple1  17936  eqgen  18597  lagsubg  18606  pgpfi  18994  sylow2alem2  19007  sylow2a  19008  sylow3lem4  19019  efgsrel  19124  odadd1  19233  odadd2  19234  gexex  19238  lt6abl  19280  dprd2d2  19431  dmdprdpr  19436  ablfacrp2  19454  ablfac1c  19458  pgpfaclem1  19468  ablfac2  19476  fincygsubgodd  19499  dvdsrmul1  19671  unitmulclb  19683  subrguss  19815  abvres  19875  znfld  20525  znunit  20528  frlmisfrlm  20810  ply1coefsupp  21216  evl1gsumadd  21274  matgsum  21334  pm2mpcl  21694  psmetxrge0  23211  isxmet2d  23225  mettri  23250  xmettri3  23251  mettri3  23252  xmetrtri2  23254  prdsxmetlem  23266  imasdsf1olem  23271  xblss2ps  23299  blss2ps  23301  blss2  23302  blssps  23322  blss  23323  prdsbl  23389  dscmet  23470  nmge0  23515  nmmtri  23520  tngngp3  23554  nlmvscnlem2  23583  nrginvrcnlem  23589  nmoix  23627  nmoleub  23629  blcvx  23695  xrsxmet  23706  opnreen  23728  xrge0tsms  23731  icopnfcnv  23839  xrhmeo  23843  lebnumii  23863  pcophtb  23926  pi1grplem  23946  nmoleub2lem  24011  ipcau2  24131  tcphcphlem1  24132  ipcau  24135  ipcnlem2  24141  rrxcph  24289  minveclem2  24323  minveclem3b  24325  pjthlem1  24334  pjthlem2  24335  ivthlem3  24350  ivth2  24352  ovolfsf  24368  ovolsslem  24381  ovollb2lem  24385  ovollb2  24386  ovolctb  24387  ovolfiniun  24398  ovolicc1  24413  ovolicc2lem4  24417  ovolicc2  24419  nulmbl2  24433  unmbl  24434  ioombl1lem4  24458  uniioombllem4  24483  uniioombllem6  24485  volivth  24504  vitalilem4  24508  itg1ge0  24583  itg1ge0a  24609  itg1lea  24610  itg1climres  24612  mbfi1fseqlem5  24617  itg2ub  24631  itg2seq  24640  itg2uba  24641  itg2splitlem  24646  itg2split  24647  itg2monolem3  24650  itg2mono  24651  itg2i1fseq2  24654  itg2addlem  24656  iblss  24702  itggt0  24741  dvferm2lem  24883  dvlip  24890  dvivthlem1  24905  dvfsumlem2  24924  dvfsumlem3  24925  ftc1lem4  24936  ply1divmo  25033  ply1remlem  25060  fta1glem2  25064  ig1pdvds  25074  plyeq0lem  25104  plydiveu  25191  fta1lem  25200  vieta1lem2  25204  aaliou3lem2  25236  aaliou3lem8  25238  ulmcn  25291  mtest  25296  itgulm  25300  radcnvlem1  25305  radcnvlt1  25310  dvradcnv  25313  pserdvlem2  25320  abelthlem2  25324  abelthlem6  25328  abelthlem7  25330  abelthlem9  25332  tangtx  25395  sinq12gt0  25397  sineq0  25413  cosordlem  25419  tanord  25427  tanregt0  25428  logrnaddcl  25463  logcj  25494  argregt0  25498  argrege0  25499  argimgt0  25500  argimlt0  25501  logimul  25502  logneg2  25503  logdivlti  25508  divlogrlim  25523  logcnlem3  25532  logcnlem4  25533  dvlog2lem  25540  logtayl  25548  rpcxpcl  25564  cxpsqrtlem  25590  cxpaddle  25638  isosctrlem1  25701  asinlem3a  25753  asinlem3  25754  asinneg  25769  asinsinlem  25774  asinsin  25775  atanlogaddlem  25796  atanlogadd  25797  atanlogsublem  25798  atanlogsub  25799  atantan  25806  atanbndlem  25808  atantayl  25820  leibpi  25825  birthdaylem3  25836  areaf  25844  cxploglim  25860  jensenlem2  25870  jensen  25871  logdiflbnd  25877  harmonicbnd4  25893  fsumharmonic  25894  zetacvg  25897  lgamgulmlem2  25912  lgamgulmlem3  25913  lgamcvg2  25937  wilthlem2  25951  wilthimp  25954  ftalem1  25955  ftalem2  25956  ftalem5  25959  basellem6  25968  basellem8  25970  basellem9  25971  chtge0  25994  chtublem  26092  logexprlim  26106  perfectlem1  26110  bcmax  26159  bposlem1  26165  bposlem2  26166  bposlem6  26170  bposlem7  26171  lgsdilem2  26214  lgsqrlem4  26230  lgsquadlem1  26261  2lgsoddprmlem2  26290  2sqlem3  26301  2sqlem8  26307  2sqblem  26312  2sqmod  26317  chebbnd1lem2  26351  chtppilimlem1  26354  chtppilim  26356  chto1ub  26357  vmadivsum  26363  rplogsumlem1  26365  rplogsumlem2  26366  dchrisum0lem1a  26367  rpvmasumlem  26368  dchrisumlem1  26370  dchrisumlem2  26371  dchrvmasumlem2  26379  dchrisum0flblem1  26389  dchrisum0flblem2  26390  dchrisum0lem1b  26396  dchrisum0lem1  26397  dchrisum0lem2a  26398  dchrisum0lem3  26400  dchrisum0  26401  mudivsum  26411  mulogsumlem  26412  mulog2sumlem1  26415  mulog2sumlem2  26416  2vmadivsumlem  26421  chpdifbndlem1  26434  selberg3lem1  26438  selberg4lem1  26441  pntrlog2bndlem1  26458  pntrlog2bndlem2  26459  pntrlog2bndlem3  26460  pntrlog2bndlem4  26461  pntpbnd1a  26466  pntpbnd1  26467  pntpbnd2  26468  pntibndlem2  26472  pntibndlem3  26473  pntlemd  26475  pntlemc  26476  pntlemb  26478  pntlemg  26479  pntlemh  26480  pntlemr  26483  pntlemf  26486  pntlemo  26488  abvcxp  26496  ostth2lem1  26499  padicabv  26511  ostth2lem2  26515  ostth2lem3  26516  ostth2lem4  26517  ostth2  26518  ostth3  26519  tgcgr4  26622  legso  26690  krippenlem  26781  midex  26828  oppperpex  26844  ttgcontlem1  26976  axpaschlem  27031  axcontlem8  27062  upgrex  27183  nbfusgrlevtxm1  27465  finsumvtxdgeven  27640  wwlksnextproplem3  27995  clwlkclwwlk2  28086  clwlkclwwlkfolem  28090  clwwlkndivn  28163  ex-ind-dvds  28544  nvabs  28753  nmooge0  28848  nmoolb  28852  siii  28934  minvecolem2  28956  minvecolem4  28961  minvecolem5  28962  hlipgt0  28995  normge0  29207  normpyc  29227  pjhthlem1  29472  pjige0i  29771  nmoplb  29988  nmfnlb  30005  branmfn  30186  pjssdif2i  30255  stlei  30321  xlt2addrd  30801  eliccelico  30818  elicoelioo  30819  bcm1n  30836  dvdszzq  30849  prmdvdsbc  30850  fsumiunle  30863  pfxlsw2ccat  30944  wrdt2ind  30945  xrge0tsmsd  31036  omndmul2  31057  psgnfzto1stlem  31086  cycpmco2lem4  31115  cycpmco2lem5  31116  cyc3conja  31143  archirngz  31162  archiabllem2c  31168  ofldchr  31232  fedgmullem2  31425  extdggt0  31446  madjusmdetlem2  31492  locfinreflem  31504  xrge0iifiso  31599  nexple  31689  gsumesum  31739  esumcst  31743  esumpcvgval  31758  esumcvg  31766  esumiun  31774  measssd  31895  measunl  31896  omssubadd  31979  carsgclctunlem3  31999  pmeasmono  32003  sibfof  32019  oddpwdc  32033  eulerpartlemgc  32041  iwrdsplit  32066  ballotlemsgt1  32189  ballotlemsel1i  32191  sgnmul  32221  signsply0  32242  signstfvc  32265  signsvtp  32274  signsvfpn  32276  fdvposlt  32291  fdvneggt  32292  fdvnegge  32294  logdivsqrle  32342  hgt750lemf  32345  tgoldbachgtde  32352  swrdwlk  32801  subfaclim  32863  erdszelem7  32872  erdszelem8  32873  cvmliftlem2  32961  snmlff  33004  sinccvglem  33343  climlec3  33417  faclim  33430  ttrcltr  33515  nodense  33632  nogt01o  33636  nosupbnd2lem1  33655  noetasuplem3  33675  cofcutr  33829  cofcutrtime  33830  fnejoin1  34294  poimirlem12  35526  poimirlem17  35531  poimirlem19  35533  poimirlem20  35534  poimirlem23  35537  poimirlem28  35542  broucube  35548  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  itg2addnclem  35565  itg2addnclem3  35567  itg2gt0cn  35569  itggt0cn  35584  ftc1anclem5  35591  ftc1anclem7  35593  ftc1anclem8  35594  isbnd3  35679  ssbnd  35683  heiborlem8  35713  bfplem2  35718  rrncmslem  35727  rrnequiv  35730  rrntotbnd  35731  lcv1  36792  lsatcv0eq  36798  lsatcvat3  36803  cvlsupr2  37094  hlatlej2  37127  cvrval4N  37165  cvratlem  37172  atcvr0eq  37177  2atlt  37190  atbtwnex  37199  athgt  37207  1cvrat  37227  ps-1  37228  hlatexch3N  37231  hlatexch4  37232  3atlem2  37235  atcvrlln2  37270  lplnexllnN  37315  4atlem3a  37348  4atlem10b  37356  4atlem11b  37359  4atlem12b  37362  2lplnja  37370  dalemply  37405  dalemsly  37406  dalem1  37410  dalem6  37419  dalem7  37420  dalem-cly  37422  dalem11  37425  dalem12  37426  dalem16  37430  dalem17  37431  dalem38  37461  dalem44  37467  dalem61  37484  lnatexN  37530  lncvrat  37533  lncmp  37534  paddasslem2  37572  dalawlem3  37624  dalawlem6  37627  dalawlem11  37632  lhpmcvr  37774  lhp2atne  37785  lhp2at0ne  37787  lautj  37844  trlval4  37939  cdlemc2  37943  cdlemc5  37946  cdleme3b  37980  cdleme11c  38012  cdleme19a  38054  cdleme20j  38069  cdleme22f  38097  cdleme23c  38102  cdleme26f2ALTN  38115  cdleme26f2  38116  cdleme35fnpq  38200  cdleme48bw  38253  cdlemg10a  38391  cdlemg11b  38393  cdlemg17g  38418  cdlemg18c  38431  cdlemi1  38569  cdlemk52  38705  dia2dimlem1  38815  dihord1  38969  dihjatcclem4  39172  lcmineqlem15  39785  lcmineqlem19  39789  lcmineqlem22  39792  aks4d1p1p4  39812  aks4d1p1p5  39816  aks4d1p2  39818  aks4d1p3  39819  sticksstones7  39830  metakunt7  39853  metakunt15  39861  metakunt16  39862  2xp3dxp2ge1d  39884  dvdsexpim  40036  dvdsexpnn0  40049  cxpgt0d  40052  prjspner01  40170  flt4lem5  40190  fltnltalem  40202  fltnlta  40203  3cubeslem1  40209  eldioph2lem1  40285  lzenom  40295  irrapxlem1  40347  irrapxlem4  40350  irrapxlem5  40351  pell14qrgt0  40384  pell1qrge1  40395  pell1qrgap  40399  pellfundge  40407  pellfundex  40411  pellfund14  40423  rmspecsqrtnq  40431  rmxypos  40472  ltrmynn0  40473  ltrmxnn0  40474  jm2.24nn  40484  jm2.17b  40486  jm2.17c  40487  jm2.24  40488  congadd  40491  congsym  40493  congneg  40494  congid  40496  mzpcong  40497  acongrep  40505  acongeq  40508  jm2.18  40513  jm2.19  40518  jm2.23  40521  jm2.25  40524  jm2.26lem3  40526  jm2.15nn0  40528  jm2.16nn0  40529  jm2.27a  40530  jm2.27c  40532  jm3.1lem1  40542  idomrootle  40723  idomsubgmo  40726  sqrtcval  40925  inductionexd  41442  imo72b2  41461  dvgrat  41603  radcnvrat  41605  binomcxplemnn0  41640  binomcxplemnotnn0  41647  cncmpmax  42248  rnmptlb  42460  zltlesub  42496  infxrpnf  42660  xrpnf  42701  fmul01  42796  fmul01lt1lem1  42800  climdivf  42828  sumnnodd  42846  climinf2lem  42922  limsup10exlem  42988  climliminf  43022  dfxlim2v  43063  xlimliminflimsup  43078  dvdivbd  43139  volge0  43177  stoweidlem1  43217  stoweidlem16  43232  stoweidlem18  43234  stoweidlem24  43240  stoweidlem26  43242  stoweidlem36  43252  stoweidlem38  43254  stoweidlem41  43257  stoweidlem42  43258  stoweidlem44  43260  stoweidlem45  43261  stoweidlem48  43264  stoweidlem62  43278  wallispilem5  43285  stirlinglem1  43290  stirlinglem5  43294  stirlinglem7  43296  stirlinglem8  43297  stirlinglem9  43298  stirlinglem11  43300  fourierdlem4  43327  fourierdlem10  43333  fourierdlem37  43360  fourierdlem47  43369  fourierdlem72  43394  fourierdlem74  43396  fourierdlem79  43401  fourierdlem82  43404  fourierdlem89  43411  fourierdlem91  43413  fourierdlem93  43415  fourierdlem103  43425  fourierdlem104  43426  fourierdlem112  43434  etransclem24  43474  etransclem25  43475  etransclem28  43478  etransclem37  43487  etransclem38  43488  etransclem44  43494  meaiuninc3v  43697  vonicclem1  43896  pimconstlt0  43913  smfsuplem1  44016  rlimdmafv  44341  rlimdmafv2  44422  2elfz2melfz  44483  iccpartgtprec  44545  iccpartlt  44549  iccpartgtl  44551  sqrtpwpw2p  44663  fmtnodvds  44669  goldbachthlem1  44670  lighneallem4a  44733  perfectALTVlem1  44846  cznnring  45187  rhmsubcrngc  45260  altgsumbcALT  45362  expnegico01  45532  flnn0div2ge  45552  rege1logbrege0  45577  fllogbd  45579  nnpw2blen  45599  nnolog2flm1  45609  dignn0ldlem  45621  dignn0flhalflem1  45634  dignn0flhalflem2  45635  eenglngeehlnmlem2  45757  itsclc0yqsol  45783  2itscp  45800  itscnhlinecirc02plem1  45801  itscnhlinecirc02plem2  45802  inlinecirc02p  45806