Theorem breqtrrd 5175

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

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  marypha1lem  9470  marypha2  9476  infsupprpr  9541  unxpwdom  9626  ttrcltr  9753  onadju  10231  nnadju  10235  cfss  10302  tskuni  10820  ltexnq  11012  lt2addmuld  12513  div4p1lem1div2  12518  nn0le2x  12577  mul2lt0rgt0  13135  prodge0ld  13140  ge2halflem1  13147  xrmax1  13213  xrmax2  13214  max1ALT  13224  qbtwnxr  13238  xleadd1a  13291  xlt2add  13298  xlesubadd  13301  xmulgt0  13321  xlemul1a  13326  xov1plusxeqvd  13534  uzsubsubfz  13582  fzctr  13676  subfzo0  13824  flflp1  13843  fldiv4lem1div2uz2  13872  ceilge  13881  modge0  13915  modlt  13916  modid  13932  m1modge3gt1  13955  modaddmodup  13971  sermono  14071  seqf1olem1  14078  seqf1olem2  14079  sqgt0  14162  sqge0  14172  leexp1a  14211  nnlesq  14240  expnbnd  14267  expmulnbnd  14270  discr1  14274  facwordi  14324  faclbnd5  14333  nfile  14394  hashdom  14414  hashgt23el  14459  fi1uzind  14542  brfi1indALT  14545  ccatws1n0  14666  swrds2  14975  cjmulge0  15181  resqrtcl  15288  absge0  15322  sqreulem  15394  amgm2  15404  rlimdm  15583  rlimge0  15613  reccn2  15629  climle  15672  climserle  15695  isercoll2  15701  iseraltlem1  15714  iseralt  15717  isumclim2  15790  isumclim3  15791  isumge0  15798  fsumless  15828  cvgcmp  15848  cvgcmpce  15850  abscvgcvg  15851  isumsup2  15878  isumltss  15880  climcndslem1  15881  climcnds  15883  supcvg  15888  harmonic  15891  expcnv  15896  explecnv  15897  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  clim2div  15921  ntrivcvgtail  15932  iprodclim2  16031  iprodclim3  16032  efcvg  16117  ege2le3  16122  efaddlem  16125  eftlub  16141  effsumlt  16143  tanhlt1  16192  ef01bndlem  16216  sin02gt0  16224  rpnnen2lem4  16249  ruclem2  16264  ruclem3  16265  ruclem9  16270  iddvdsexp  16313  dvdsadd  16335  dvdsfac  16359  dvdsexp2im  16360  dvdsmod  16362  3dvds  16364  omoe  16397  sumeven  16420  divalglem1  16427  flodddiv4t2lthalf  16451  bitsfzo  16468  bitsmod  16469  bitscmp  16471  bitsinv1lem  16474  sadcaddlem  16490  sadadd3  16494  sadaddlem  16499  dvdssqim  16587  dvdsexpim  16588  dvdsmulgcd  16589  nn0seqcvgd  16603  dvdslcm  16631  lcmgcdlem  16639  dvdslcmf  16664  lcmfunsnlem2lem2  16672  mulgcddvds  16688  qredeq  16690  cncongr2  16701  sqnprm  16735  isprm6  16747  dvdszzq  16754  prmdvdsbc  16759  nonsq  16792  hashdvds  16808  prmdiv  16818  odzdvds  16828  pythagtriplem4  16852  pcpre1  16875  pcdvdsb  16902  pcz  16914  pcprmpw2  16915  pcaddlem  16921  pcadd  16922  pcadd2  16923  pcmpt  16925  pcmptdvds  16927  fldivp1  16930  pcfaclem  16931  pockthlem  16938  prmreclem1  16949  prmreclem3  16951  prmreclem5  16953  prmreclem6  16954  4sqlem6  16976  4sqlem8  16978  4sqlem11  16988  4sqlem12  16989  4sqlem14  16991  4sqlem16  16993  vdwlem3  17016  vdwlem9  17022  vdwlem10  17023  vdwlem12  17025  ramub1lem2  17060  prmgap  17092  prmgaplcm  17093  prmgapprmo  17095  mreexexd  17692  invfuc  18030  ple1  18487  eqgen  19211  lagsubg  19225  pgpfi  19637  sylow2alem2  19650  sylow2a  19651  sylow3lem4  19662  efgsrel  19766  odadd1  19880  odadd2  19881  gexex  19885  lt6abl  19927  dprd2d2  20078  dmdprdpr  20083  ablfacrp2  20101  ablfac1c  20105  pgpfaclem1  20115  ablfac2  20123  fincygsubgodd  20146  dvdsrmul1  20385  unitmulclb  20397  subrguss  20603  rhmsubcrngc  20684  abvres  20848  znfld  21596  znunit  21599  frlmisfrlm  21885  ply1coefsupp  22316  evl1gsumadd  22377  matgsum  22458  pm2mpcl  22818  psmetxrge0  24338  isxmet2d  24352  mettri  24377  xmettri3  24378  mettri3  24379  xmetrtri2  24381  prdsxmetlem  24393  imasdsf1olem  24398  xblss2ps  24426  blss2ps  24428  blss2  24429  blssps  24449  blss  24450  prdsbl  24519  dscmet  24600  nmge0  24645  nmmtri  24650  tngngp3  24692  nlmvscnlem2  24721  nrginvrcnlem  24727  nmoix  24765  nmoleub  24767  blcvx  24833  xrsxmet  24844  opnreen  24866  xrge0tsms  24869  icopnfcnv  24986  xrhmeo  24990  lebnumii  25011  pcophtb  25075  pi1grplem  25095  nmoleub2lem  25160  ipcau2  25281  tcphcphlem1  25282  ipcau  25285  ipcnlem2  25291  rrxcph  25439  minveclem2  25473  minveclem3b  25475  pjthlem1  25484  pjthlem2  25485  ivthlem3  25501  ivth2  25503  ovolfsf  25519  ovolsslem  25532  ovollb2lem  25536  ovollb2  25537  ovolctb  25538  ovolfiniun  25549  ovolicc1  25564  ovolicc2lem4  25568  ovolicc2  25570  nulmbl2  25584  unmbl  25585  ioombl1lem4  25609  uniioombllem4  25634  uniioombllem6  25636  volivth  25655  vitalilem4  25659  itg1ge0  25734  itg1ge0a  25760  itg1lea  25761  itg1climres  25763  mbfi1fseqlem5  25768  itg2ub  25782  itg2seq  25791  itg2uba  25792  itg2splitlem  25797  itg2split  25798  itg2monolem3  25801  itg2mono  25802  itg2i1fseq2  25805  itg2addlem  25807  iblss  25854  itggt0  25893  dvferm2lem  26038  dvlip  26046  dvivthlem1  26061  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  ftc1lem4  26094  ply1divmo  26189  ply1remlem  26218  fta1glem2  26222  idomrootle  26226  ig1pdvds  26233  plyeq0lem  26263  plydiveu  26354  fta1lem  26363  vieta1lem2  26367  aaliou3lem2  26399  aaliou3lem8  26401  ulmcn  26456  mtest  26461  itgulm  26465  radcnvlem1  26470  radcnvlt1  26475  dvradcnv  26478  pserdvlem2  26486  abelthlem2  26490  abelthlem6  26494  abelthlem7  26496  abelthlem9  26498  tangtx  26561  sinq12gt0  26563  sineq0  26580  cosordlem  26586  tanord  26594  tanregt0  26595  logrnaddcl  26630  logcj  26662  argregt0  26666  argrege0  26667  argimgt0  26668  argimlt0  26669  logimul  26670  logneg2  26671  logdivlti  26676  divlogrlim  26691  logcnlem3  26700  logcnlem4  26701  dvlog2lem  26708  logtayl  26716  rpcxpcl  26732  cxpsqrtlem  26758  cxpaddle  26809  isosctrlem1  26875  asinlem3a  26927  asinlem3  26928  asinneg  26943  asinsinlem  26948  asinsin  26949  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atanlogsub  26973  atantan  26980  atanbndlem  26982  atantayl  26994  leibpi  26999  birthdaylem3  27010  areaf  27018  cxploglim  27035  jensenlem2  27045  jensen  27046  logdiflbnd  27052  harmonicbnd4  27068  fsumharmonic  27069  zetacvg  27072  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamcvg2  27112  wilthlem2  27126  wilthimp  27129  ftalem1  27130  ftalem2  27131  ftalem5  27134  basellem6  27143  basellem8  27145  basellem9  27146  chtge0  27169  chtublem  27269  logexprlim  27283  perfectlem1  27287  bcmax  27336  bposlem1  27342  bposlem2  27343  bposlem6  27347  bposlem7  27348  lgsdilem2  27391  lgsqrlem4  27407  lgsquadlem1  27438  2lgsoddprmlem2  27467  2sqlem3  27478  2sqlem8  27484  2sqblem  27489  2sqmod  27494  chebbnd1lem2  27528  chtppilimlem1  27531  chtppilim  27533  chto1ub  27534  vmadivsum  27540  rplogsumlem1  27542  rplogsumlem2  27543  dchrisum0lem1a  27544  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrvmasumlem2  27556  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem3  27577  dchrisum0  27578  mudivsum  27588  mulogsumlem  27589  mulog2sumlem1  27592  mulog2sumlem2  27593  2vmadivsumlem  27598  chpdifbndlem1  27611  selberg3lem1  27615  selberg4lem1  27618  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntibndlem3  27650  pntlemd  27652  pntlemc  27653  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemr  27660  pntlemf  27663  pntlemo  27665  abvcxp  27673  ostth2lem1  27676  padicabv  27688  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth2  27695  ostth3  27696  nodense  27751  nogt01o  27755  nosupbnd2lem1  27774  noetasuplem3  27794  maxs1  27824  maxs2  27825  cofcutr  27972  cofcutrtime  27975  addsuniflem  28048  negsunif  28101  ssltmul2  28188  precsexlem11  28255  abssge0  28283  sleabs  28286  om2noseqlt  28319  expsgt0  28429  halfcut  28430  addhalfcut  28433  tgcgr4  28553  legso  28621  krippenlem  28712  midex  28759  oppperpex  28775  ttgcontlem1  28913  axpaschlem  28969  axcontlem8  29000  upgrex  29123  nbfusgrlevtxm1  29408  finsumvtxdgeven  29584  wwlksnextproplem3  29940  clwlkclwwlk2  30031  clwlkclwwlkfolem  30035  clwwlkndivn  30108  ex-ind-dvds  30489  nvabs  30700  nmooge0  30795  nmoolb  30799  siii  30881  minvecolem2  30903  minvecolem4  30908  minvecolem5  30909  hlipgt0  30942  normge0  31154  normpyc  31174  pjhthlem1  31419  pjige0i  31718  nmoplb  31935  nmfnlb  31952  branmfn  32133  pjssdif2i  32202  stlei  32268  xlt2addrd  32768  eliccelico  32785  elicoelioo  32786  bcm1n  32802  fsumiunle  32835  ccatdmss  32918  pfxlsw2ccat  32919  wrdt2ind  32922  chnub  32985  xrge0tsmsd  33047  gsumwrd2dccatlem  33051  omndmul2  33071  psgnfzto1stlem  33102  cycpmco2lem4  33131  cycpmco2lem5  33132  cyc3conja  33159  archirngz  33178  archiabllem2c  33184  ofldchr  33323  rprmasso2  33533  rprmirred  33538  1arithufdlem3  33553  fedgmullem2  33657  extdggt0  33684  evls1fldgencl  33694  algextdeglem8  33729  rtelextdg2lem  33731  madjusmdetlem2  33788  locfinreflem  33800  xrge0iifiso  33895  nexple  33989  gsumesum  34039  esumcst  34043  esumpcvgval  34058  esumcvg  34066  esumiun  34074  measssd  34195  measunl  34196  omssubadd  34281  carsgclctunlem3  34301  pmeasmono  34305  sibfof  34321  oddpwdc  34335  eulerpartlemgc  34343  iwrdsplit  34368  ballotlemsgt1  34491  ballotlemsel1i  34493  sgnmul  34523  signsply0  34544  signstfvc  34567  signsvtp  34576  signsvfpn  34578  fdvposlt  34592  fdvneggt  34593  fdvnegge  34595  logdivsqrle  34643  hgt750lemf  34646  tgoldbachgtde  34653  swrdwlk  35110  subfaclim  35172  erdszelem7  35181  erdszelem8  35182  cvmliftlem2  35270  snmlff  35313  sinccvglem  35656  climlec3  35713  faclim  35725  fnejoin1  36350  poimirlem12  37618  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem23  37629  poimirlem28  37634  broucube  37640  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  itg2addnclem3  37659  itg2gt0cn  37661  itggt0cn  37676  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  isbnd3  37770  ssbnd  37774  heiborlem8  37804  bfplem2  37809  rrncmslem  37818  rrnequiv  37821  rrntotbnd  37822  lcv1  39022  lsatcv0eq  39028  lsatcvat3  39033  cvlsupr2  39324  hlatlej2  39357  cvrval4N  39396  cvratlem  39403  atcvr0eq  39408  2atlt  39421  atbtwnex  39430  athgt  39438  1cvrat  39458  ps-1  39459  hlatexch3N  39462  hlatexch4  39463  3atlem2  39466  atcvrlln2  39501  lplnexllnN  39546  4atlem3a  39579  4atlem10b  39587  4atlem11b  39590  4atlem12b  39593  2lplnja  39601  dalemply  39636  dalemsly  39637  dalem1  39641  dalem6  39650  dalem7  39651  dalem-cly  39653  dalem11  39656  dalem12  39657  dalem16  39661  dalem17  39662  dalem38  39692  dalem44  39698  dalem61  39715  lnatexN  39761  lncvrat  39764  lncmp  39765  paddasslem2  39803  dalawlem3  39855  dalawlem6  39858  dalawlem11  39863  lhpmcvr  40005  lhp2atne  40016  lhp2at0ne  40018  lautj  40075  trlval4  40170  cdlemc2  40174  cdlemc5  40177  cdleme3b  40211  cdleme11c  40243  cdleme19a  40285  cdleme20j  40300  cdleme22f  40328  cdleme23c  40333  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme35fnpq  40431  cdleme48bw  40484  cdlemg10a  40622  cdlemg11b  40624  cdlemg17g  40649  cdlemg18c  40662  cdlemi1  40800  cdlemk52  40936  dia2dimlem1  41046  dihord1  41200  dihjatcclem4  41403  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  metakunt7  42192  metakunt15  42200  metakunt16  42201  2xp3dxp2ge1d  42222  dvdsexpnn0  42347  prjspner01  42611  flt4lem5  42636  fltnltalem  42648  fltnlta  42649  3cubeslem1  42671  eldioph2lem1  42747  lzenom  42757  irrapxlem1  42809  irrapxlem4  42812  irrapxlem5  42813  pell14qrgt0  42846  pell1qrge1  42857  pell1qrgap  42861  pellfundge  42869  pellfundex  42873  pellfund14  42885  rmspecsqrtnq  42893  rmxypos  42935  ltrmynn0  42936  ltrmxnn0  42937  jm2.24nn  42947  jm2.17b  42949  jm2.17c  42950  jm2.24  42951  congadd  42954  congsym  42956  congneg  42957  congid  42959  mzpcong  42960  acongrep  42968  acongeq  42971  jm2.18  42976  jm2.19  42981  jm2.23  42984  jm2.25  42987  jm2.26lem3  42989  jm2.15nn0  42991  jm2.16nn0  42992  jm2.27a  42993  jm2.27c  42995  jm3.1lem1  43005  idomsubgmo  43181  sqrtcval  43630  inductionexd  44144  imo72b2lem0  44154  imo72b2  44161  dvgrat  44307  radcnvrat  44309  binomcxplemnn0  44344  binomcxplemnotnn0  44351  cncmpmax  44969  rnmptlb  45187  zltlesub  45235  infxrpnf  45395  xrpnf  45435  fmul01  45535  fmul01lt1lem1  45539  climdivf  45567  sumnnodd  45585  climinf2lem  45661  limsup10exlem  45727  climliminf  45761  dfxlim2v  45802  xlimliminflimsup  45817  dvdivbd  45878  volge0  45916  stoweidlem1  45956  stoweidlem16  45971  stoweidlem18  45973  stoweidlem24  45979  stoweidlem26  45981  stoweidlem36  45991  stoweidlem38  45993  stoweidlem41  45996  stoweidlem42  45997  stoweidlem44  45999  stoweidlem45  46000  stoweidlem48  46003  stoweidlem62  46017  wallispilem5  46024  stirlinglem1  46029  stirlinglem5  46033  stirlinglem7  46035  stirlinglem8  46036  stirlinglem9  46037  stirlinglem11  46039  fourierdlem4  46066  fourierdlem10  46072  fourierdlem37  46099  fourierdlem47  46108  fourierdlem72  46133  fourierdlem74  46135  fourierdlem79  46140  fourierdlem82  46143  fourierdlem89  46150  fourierdlem91  46152  fourierdlem93  46154  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  etransclem24  46213  etransclem25  46214  etransclem28  46217  etransclem37  46226  etransclem38  46227  etransclem44  46233  meaiuninc3v  46439  vonicclem1  46638  pimconstlt0  46656  smfsuplem1  46766  rlimdmafv  47126  rlimdmafv2  47207  2elfz2melfz  47267  iccpartgtprec  47344  iccpartlt  47348  iccpartgtl  47350  sqrtpwpw2p  47462  fmtnodvds  47468  goldbachthlem1  47469  lighneallem4a  47532  perfectALTVlem1  47645  uhgrimgrlim  47889  cznnring  48105  altgsumbcALT  48197  expnegico01  48363  flnn0div2ge  48382  rege1logbrege0  48407  fllogbd  48409  nnpw2blen  48429  nnolog2flm1  48439  dignn0ldlem  48451  dignn0flhalflem1  48464  dignn0flhalflem2  48465  eenglngeehlnmlem2  48587  itsclc0yqsol  48613  2itscp  48630  itscnhlinecirc02plem1  48631  itscnhlinecirc02plem2  48632  inlinecirc02p  48636