Theorem breqtrrd 5142

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5112

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5113

This theorem is used by:  marypha1lem  9395  marypha2  9401  infsupprpr  9468  unxpwdom  9553  ttrcltr  9687  onadju  10188  nnadju  10192  cfss  10259  tskuni  10778  ltexnq  10970  lt2addmuld  12504  div4p1lem1div2  12509  nn0le2x  12568  mul2lt0rgt0  13131  prodge0ld  13136  ge2halflem1  13143  xrmax1  13211  xrmax2  13212  max1ALT  13222  qbtwnxr  13236  xleadd1a  13289  xlt2add  13296  xlesubadd  13299  xmulgt0  13319  xlemul1a  13324  xov1plusxeqvd  13535  uzsubsubfz  13585  fzctr  13679  subfzo0  13832  flflp1  13851  fldiv4lem1div2uz2  13880  ceilge  13889  modge0  13923  modlt  13924  modid  13940  m1modge3gt1  13965  modaddmodup  13981  sermono  14081  seqf1olem1  14088  seqf1olem2  14089  sqgt0  14173  sqge0  14183  leexp1a  14222  nnlesq  14252  expnbnd  14279  expmulnbnd  14282  discr1  14286  facwordi  14336  faclbnd5  14345  nfile  14406  hashdom  14426  hashgt23el  14472  fi1uzind  14555  brfi1indALT  14558  ccatdmss  14630  ccatws1n0  14681  swrds2  14988  sgnmul  15155  cjmulge0  15208  resqrtcl  15315  absge0  15349  sqreulem  15422  amgm2  15432  rlimdm  15613  rlimge0  15643  reccn2  15659  climle  15702  climserle  15725  isercoll2  15731  iseraltlem1  15744  iseralt  15747  isumclim2  15820  isumclim3  15821  isumge0  15828  fsumless  15859  cvgcmp  15879  cvgcmpce  15881  abscvgcvg  15882  isumsup2  15911  isumltss  15913  climcndslem1  15914  climcnds  15916  supcvg  15921  harmonic  15924  expcnv  15929  explecnv  15930  cvgrat  15948  mertenslem1  15949  mertenslem2  15950  clim2div  15954  ntrivcvgtail  15965  iprodclim2  16064  iprodclim3  16065  efcvg  16149  ege2le3  16154  efaddlem  16157  eftlub  16175  effsumlt  16177  tanhlt1  16226  ef01bndlem  16250  sin02gt0  16258  rpnnen2lem4  16283  ruclem2  16298  ruclem3  16299  ruclem9  16304  iddvdsexp  16347  dvdsadd  16370  dvdsfac  16394  dvdsexp2im  16395  dvdsmod  16397  3dvds  16399  omoe  16432  sumeven  16455  divalglem1  16462  flodddiv4t2lthalf  16486  bitsfzo  16503  bitsmod  16504  bitscmp  16506  bitsinv1lem  16509  sadcaddlem  16525  sadadd3  16529  sadaddlem  16534  dvdssqim  16622  dvdsexpim  16623  dvdsmulgcd  16624  nn0seqcvgd  16638  dvdslcm  16666  lcmgcdlem  16674  dvdslcmf  16699  lcmfunsnlem2lem2  16707  mulgcddvds  16723  qredeq  16725  cncongr2  16736  sqnprm  16771  isprm6  16783  dvdszzq  16790  prmdvdsbc  16795  nonsq  16828  hashdvds  16844  prmdiv  16854  odzdvds  16865  pythagtriplem4  16889  pcpre1  16912  pcdvdsb  16939  pcz  16951  pcprmpw2  16952  pcaddlem  16958  pcadd  16959  pcadd2  16960  pcmpt  16962  pcmptdvds  16964  fldivp1  16967  pcfaclem  16968  pockthlem  16975  prmreclem1  16986  prmreclem3  16988  prmreclem5  16990  prmreclem6  16991  4sqlem6  17013  4sqlem8  17015  4sqlem11  17025  4sqlem12  17026  4sqlem14  17028  4sqlem16  17030  vdwlem3  17053  vdwlem9  17059  vdwlem10  17060  vdwlem12  17062  ramub1lem2  17097  prmgap  17129  prmgaplcm  17130  prmgapprmo  17132  mreexexd  17714  invfuc  18044  ple1  18494  chnub  18688  eqgen  19259  lagsubg  19276  pgpfi  19685  sylow2alem2  19698  sylow2a  19699  sylow3lem4  19710  efgsrel  19814  odadd1  19928  odadd2  19929  gexex  19933  lt6abl  19975  dprd2d2  20126  dmdprdpr  20131  ablfacrp2  20149  ablfac1c  20153  pgpfaclem1  20163  ablfac2  20171  fincygsubgodd  20194  omndmul2  20213  dvdsrmul1  20462  unitmulclb  20474  subrguss  20701  rhmsubcrngc  20782  abvres  20949  znfld  21725  znunit  21728  ofldchr  21741  frlmisfrlm  22013  ply1coefsupp  22472  evl1gsumadd  22533  matgsum  22609  pm2mpcl  22969  psmetxrge0  24485  isxmet2d  24499  mettri  24524  xmettri3  24525  mettri3  24526  xmetrtri2  24528  prdsxmetlem  24540  imasdsf1olem  24545  xblss2ps  24573  blss2ps  24575  blss2  24576  blssps  24596  blss  24597  prdsbl  24663  dscmet  24744  nmge0  24789  nmmtri  24794  tngngp3  24828  nlmvscnlem2  24857  nrginvrcnlem  24863  nmoix  24901  nmoleub  24903  blcvx  24970  xrsxmet  24982  opnreen  25004  xrge0tsms  25007  icopnfcnv  25116  xrhmeo  25120  lebnumii  25140  pcophtb  25203  pi1grplem  25223  nmoleub2lem  25288  ipcau2  25408  tcphcphlem1  25409  ipcau  25412  ipcnlem2  25418  rrxcph  25566  minveclem2  25600  minveclem3b  25602  pjthlem1  25611  pjthlem2  25612  ivthlem3  25627  ivth2  25629  ovolfsf  25645  ovolsslem  25658  ovollb2lem  25662  ovollb2  25663  ovolctb  25664  ovolfiniun  25675  ovolicc1  25690  ovolicc2lem4  25694  ovolicc2  25696  nulmbl2  25710  unmbl  25711  ioombl1lem4  25735  uniioombllem4  25760  uniioombllem6  25762  volivth  25781  vitalilem4  25785  itg1ge0  25860  itg1ge0a  25885  itg1lea  25886  itg1climres  25888  mbfi1fseqlem5  25893  itg2ub  25907  itg2seq  25916  itg2uba  25917  itg2splitlem  25922  itg2split  25923  itg2monolem3  25926  itg2mono  25927  itg2i1fseq2  25930  itg2addlem  25932  iblss  25979  itggt0  26018  dvferm2lem  26160  dvlip  26167  dvivthlem1  26182  dvfsumlem2  26201  dvfsumlem3  26202  ftc1lem4  26213  ply1divmo  26308  ply1remlem  26337  fta1glem2  26341  idomrootle  26345  ig1pdvds  26352  plyeq0lem  26382  plydiveu  26474  fta1lem  26483  vieta1lem2  26487  aaliou3lem2  26521  aaliou3lem8  26523  ulmcn  26577  mtest  26582  itgulm  26586  radcnvlem1  26591  radcnvlt1  26596  dvradcnv  26599  pserdvlem2  26606  abelthlem2  26610  abelthlem6  26614  abelthlem7  26616  abelthlem9  26618  tangtx  26685  sinq12gt0  26687  sineq0  26704  cosordlem  26710  tanord  26718  tanregt0  26719  logrnaddcl  26754  logcj  26786  argregt0  26790  argrege0  26791  argimgt0  26792  argimlt0  26793  logimul  26794  logneg2  26795  logdivlti  26800  divlogrlim  26815  logcnlem3  26824  logcnlem4  26825  dvlog2lem  26832  logtayl  26840  rpcxpcl  26856  cxpsqrtlem  26882  cxpaddle  26932  isosctrlem1  26998  asinlem3a  27050  asinlem3  27051  asinneg  27066  asinsinlem  27071  asinsin  27072  atanlogaddlem  27093  atanlogadd  27094  atanlogsublem  27095  atanlogsub  27096  atantan  27103  atanbndlem  27105  atantayl  27117  leibpi  27122  birthdaylem3  27133  areaf  27141  cxploglim  27157  jensenlem2  27167  jensen  27168  logdiflbnd  27174  harmonicbnd4  27190  fsumharmonic  27191  zetacvg  27194  lgamgulmlem2  27209  lgamgulmlem3  27210  lgamcvg2  27234  wilthlem2  27248  wilthimp  27251  ftalem1  27252  ftalem2  27253  ftalem5  27256  basellem6  27265  basellem8  27267  basellem9  27268  chtge0  27291  chtublem  27390  logexprlim  27404  perfectlem1  27408  bcmax  27457  bposlem1  27463  bposlem2  27464  bposlem6  27468  bposlem7  27469  lgsdilem2  27512  lgsqrlem4  27528  lgsquadlem1  27559  2lgsoddprmlem2  27588  2sqlem3  27599  2sqlem8  27605  2sqblem  27610  2sqmod  27615  chebbnd1lem2  27649  chtppilimlem1  27652  chtppilim  27654  chto1ub  27655  vmadivsum  27661  rplogsumlem1  27663  rplogsumlem2  27664  dchrisum0lem1a  27665  rpvmasumlem  27666  dchrisumlem1  27668  dchrisumlem2  27669  dchrvmasumlem2  27677  dchrisum0flblem1  27687  dchrisum0flblem2  27688  dchrisum0lem1b  27694  dchrisum0lem1  27695  dchrisum0lem2a  27696  dchrisum0lem3  27698  dchrisum0  27699  mudivsum  27709  mulogsumlem  27710  mulog2sumlem1  27713  mulog2sumlem2  27714  2vmadivsumlem  27719  chpdifbndlem1  27732  selberg3lem1  27736  selberg4lem1  27739  pntrlog2bndlem1  27756  pntrlog2bndlem2  27757  pntrlog2bndlem3  27758  pntrlog2bndlem4  27759  pntpbnd1a  27764  pntpbnd1  27765  pntpbnd2  27766  pntibndlem2  27770  pntibndlem3  27771  pntlemd  27773  pntlemc  27774  pntlemb  27776  pntlemg  27777  pntlemh  27778  pntlemr  27781  pntlemf  27784  pntlemo  27786  abvcxp  27794  ostth2lem1  27797  padicabv  27809  ostth2lem2  27813  ostth2lem3  27814  ostth2lem4  27815  ostth2  27816  ostth3  27817  nodense  27871  nogt01o  27875  nosupbnd2lem1  27894  noetasuplem3  27914  maxs1  27948  maxs2  27949  eqcuts3  28012  cofcutr  28132  cofcutrtime  28135  addsuniflem  28209  negsunif  28263  sltmuls2  28356  precsexlem11  28425  abssge0  28453  leabss  28456  oncutlt  28472  om2noseqlt  28507  zsoring  28617  expsgt0  28645  halfcut  28666  addhalfcut  28667  bdayfinbndlem1  28675  elreno2  28703  tgcgr4  28815  legso  28883  krippenlem  28982  midex  29033  oppperpex  29049  prlngmid2  29226  prlngsymquadopp  29230  quadcgrprlng  29231  ttgcontlem1  29249  axpaschlem  29305  axcontlem8  29336  upgrex  29457  nbfusgrlevtxm1  29742  finsumvtxdgeven  29917  wwlksnextproplem3  30275  clwlkclwwlk2  30369  clwlkclwwlkfolem  30373  clwwlkndivn  30446  ex-ind-dvds  30827  nvabs  31039  nmooge0  31134  nmoolb  31138  siii  31220  minvecolem2  31242  minvecolem4  31247  minvecolem5  31248  hlipgt0  31281  normge0  31493  normpyc  31513  pjhthlem1  31758  pjige0i  32057  nmoplb  32274  nmfnlb  32291  branmfn  32472  pjssdif2i  32541  stlei  32607  xlt2addrd  33119  eliccelico  33137  elicoelioo  33138  bcm1n  33155  fsumiunle  33188  nexple  33192  expevenpos  33194  pfxlsw2ccat  33283  wrdt2ind  33286  xrge0tsmsd  33406  gsumwrd2dccatlem  33410  psgnfzto1stlem  33433  cycpmco2lem4  33462  cycpmco2lem5  33463  cyc3conja  33490  archirngz  33522  archiabllem2c  33528  rprmasso2  33829  rprmirred  33834  1arithufdlem3  33849  vietadeg1  33981  lbslelsp  34001  fedgmullem2  34033  extdggt0  34060  evls1fldgencl  34073  fldextrspunlem1  34078  extdgfialglem1  34095  algextdeglem8  34127  rtelextdg2lem  34129  cos9thpiminplylem1  34185  cos9thpiminplylem2  34186  madjusmdetlem2  34231  locfinreflem  34243  xrge0iifiso  34338  gsumesum  34462  esumcst  34466  esumpcvgval  34481  esumcvg  34489  esumiun  34497  measssd  34618  measunl  34619  omssubadd  34703  carsgclctunlem3  34723  pmeasmono  34727  sibfof  34743  oddpwdc  34757  eulerpartlemgc  34765  iwrdsplit  34790  ballotlemsgt1  34914  ballotlemsel1i  34916  signsply0  34951  signstfvc  34974  signsvtp  34983  signsvfpn  34985  fdvposlt  34999  fdvneggt  35000  fdvnegge  35002  logdivsqrle  35050  hgt750lemf  35053  tgoldbachgtde  35060  swrdwlk  35631  subfaclim  35692  erdszelem7  35701  erdszelem8  35702  cvmliftlem2  35790  snmlff  35833  sinccvglem  36176  climlec3  36238  faclim  36250  fnejoin1  36911  poimirlem12  38315  poimirlem17  38320  poimirlem19  38322  poimirlem20  38323  poimirlem23  38326  poimirlem28  38331  broucube  38337  mblfinlem2  38341  mblfinlem3  38342  mblfinlem4  38343  ismblfin  38344  itg2addnclem  38354  itg2addnclem3  38356  itg2gt0cn  38358  itggt0cn  38373  ftc1anclem5  38380  ftc1anclem7  38382  ftc1anclem8  38383  isbnd3  38467  ssbnd  38471  heiborlem8  38501  bfplem2  38506  rrncmslem  38515  rrnequiv  38518  rrntotbnd  38519  lcv1  39847  lsatcv0eq  39853  lsatcvat3  39858  cvlsupr2  40149  hlatlej2  40182  cvrval4N  40220  cvratlem  40227  atcvr0eq  40232  2atlt  40245  atbtwnex  40254  athgt  40262  1cvrat  40282  ps-1  40283  hlatexch3N  40286  hlatexch4  40287  3atlem2  40290  atcvrlln2  40325  lplnexllnN  40370  4atlem3a  40403  4atlem10b  40411  4atlem11b  40414  4atlem12b  40417  2lplnja  40425  dalemply  40460  dalemsly  40461  dalem1  40465  dalem6  40474  dalem7  40475  dalem-cly  40477  dalem11  40480  dalem12  40481  dalem16  40485  dalem17  40486  dalem38  40516  dalem44  40522  dalem61  40539  lnatexN  40585  lncvrat  40588  lncmp  40589  paddasslem2  40627  dalawlem3  40679  dalawlem6  40682  dalawlem11  40687  lhpmcvr  40829  lhp2atne  40840  lhp2at0ne  40842  lautj  40899  trlval4  40994  cdlemc2  40998  cdlemc5  41001  cdleme3b  41035  cdleme11c  41067  cdleme19a  41109  cdleme20j  41124  cdleme22f  41152  cdleme23c  41157  cdleme26f2ALTN  41170  cdleme26f2  41171  cdleme35fnpq  41255  cdleme48bw  41308  cdlemg10a  41446  cdlemg11b  41448  cdlemg17g  41473  cdlemg18c  41486  cdlemi1  41624  cdlemk52  41760  dia2dimlem1  41870  dihord1  42024  dihjatcclem4  42227  lcmineqlem15  42842  lcmineqlem19  42846  lcmineqlem22  42849  aks4d1lem1  42861  aks4d1p1p4  42870  aks4d1p1p5  42874  aks4d1p2  42876  aks4d1p3  42877  aks4d1p6  42880  aks4d1p7d1  42881  aks4d1p7  42882  aks4d1p8  42886  aks4d1p9  42887  aks6d1c1p6  42913  aks6d1c1  42915  aks6d1c2  42929  sticksstones7  42951  aks6d1c7lem1  42979  unitscyglem4  42997  dvdsexpnn0  43127  prjspner01  43389  flt4lem5  43414  fltnltalem  43426  fltnlta  43427  3cubeslem1  43447  eldioph2lem1  43523  lzenom  43533  irrapxlem1  43581  irrapxlem4  43584  irrapxlem5  43585  pell14qrgt0  43618  pell1qrge1  43629  pell1qrgap  43633  pellfundge  43641  pellfundex  43645  pellfund14  43657  rmspecsqrtnq  43665  rmxypos  43706  ltrmynn0  43707  ltrmxnn0  43708  jm2.24nn  43718  jm2.17b  43720  jm2.17c  43721  jm2.24  43722  congadd  43725  congsym  43727  congneg  43728  congid  43730  mzpcong  43731  acongrep  43739  acongeq  43742  jm2.18  43747  jm2.19  43752  jm2.23  43755  jm2.25  43758  jm2.26lem3  43760  jm2.15nn0  43762  jm2.16nn0  43763  jm2.27a  43764  jm2.27c  43766  jm3.1lem1  43776  idomsubgmo  43952  sqrtcval  44399  inductionexd  44913  imo72b2lem0  44923  imo72b2  44930  dvgrat  45054  radcnvrat  45056  binomcxplemnn0  45091  binomcxplemnotnn0  45098  cncmpmax  45784  rnmptlb  45990  zltlesub  46036  infxrpnf  46192  xrpnf  46231  fmul01  46328  fmul01lt1lem1  46332  climdivf  46360  sumnnodd  46378  climinf2lem  46452  limsup10exlem  46518  climliminf  46552  dfxlim2v  46593  xlimliminflimsup  46608  dvdivbd  46669  volge0  46707  stoweidlem1  46747  stoweidlem16  46762  stoweidlem18  46764  stoweidlem24  46770  stoweidlem26  46772  stoweidlem36  46782  stoweidlem38  46784  stoweidlem41  46787  stoweidlem42  46788  stoweidlem44  46790  stoweidlem45  46791  stoweidlem48  46794  stoweidlem62  46808  wallispilem5  46815  stirlinglem1  46820  stirlinglem5  46824  stirlinglem7  46826  stirlinglem8  46827  stirlinglem9  46828  stirlinglem11  46830  fourierdlem4  46857  fourierdlem10  46863  fourierdlem37  46890  fourierdlem47  46899  fourierdlem72  46924  fourierdlem74  46926  fourierdlem79  46931  fourierdlem82  46934  fourierdlem89  46941  fourierdlem91  46943  fourierdlem93  46945  fourierdlem103  46955  fourierdlem104  46956  fourierdlem112  46964  etransclem24  47004  etransclem25  47005  etransclem28  47008  etransclem37  47017  etransclem38  47018  etransclem44  47024  meaiuninc3v  47230  vonicclem1  47429  pimconstlt0  47447  smfsuplem1  47557  chnerlem1  47630  rlimdmafv  47946  rlimdmafv2  48027  2elfz2melfz  48087  2timesltsq  48147  muldvdsfacgt  48155  iccpartgtprec  48201  iccpartlt  48205  iccpartgtl  48207  sqrtpwpw2p  48322  fmtnodvds  48328  goldbachthlem1  48329  lighneallem4a  48392  nprmdvdsfacm1lem1  48404  perfectALTVlem1  48518  uhgrimgrlim  48784  cznnring  49059  altgsumbcALT  49165  expnegico01  49330  flnn0div2ge  49345  rege1logbrege0  49370  fllogbd  49372  nnpw2blen  49392  nnolog2flm1  49402  dignn0ldlem  49414  dignn0flhalflem1  49427  dignn0flhalflem2  49428  eenglngeehlnmlem2  49550  itsclc0yqsol  49576  2itscp  49593  itscnhlinecirc02plem1  49594  itscnhlinecirc02plem2  49595  inlinecirc02p  49599