Theorem breqtrrd 4996

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

Syntax hints:   → wi 4   = wceq 1525   class class class wbr 4968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969

This theorem is referenced by:  marypha1lem  8750  marypha2  8756  infsupprpr  8821  unxpwdom  8906  onadju  9472  cfss  9540  tskuni  10058  ltexnq  10250  lt2addmuld  11741  div4p1lem1div2  11746  mul2lt0rgt0  12346  prodge0ld  12351  xrmax1  12422  xrmax2  12423  max1ALT  12433  qbtwnxr  12447  xleadd1a  12500  xlt2add  12507  xlesubadd  12510  xmulgt0  12530  xlemul1a  12535  xov1plusxeqvd  12738  uzsubsubfz  12783  fzctr  12873  subfzo0  13013  flflp1  13031  fldiv4lem1div2uz2  13060  ceilge  13068  modge0  13101  modlt  13102  modid  13118  m1modge3gt1  13140  modaddmodup  13156  sermono  13256  seqf1olem1  13263  seqf1olem2  13264  sqgt0  13345  sqge0  13355  leexp1a  13393  nnlesq  13422  expnbnd  13447  expmulnbnd  13450  discr1  13454  facwordi  13503  faclbnd5  13512  nfile  13574  hashdom  13592  hashgt23el  13637  fi1uzind  13705  brfi1indALT  13708  ccatws1n0  13834  swrds2  14142  cjmulge0  14343  resqrtcl  14451  absge0  14485  sqreulem  14557  amgm2  14567  rlimdm  14746  rlimge0  14776  reccn2  14791  climle  14834  climserle  14857  isercoll2  14863  iseraltlem1  14876  iseralt  14879  isumclim2  14950  isumclim3  14951  isumge0  14958  fsumless  14988  cvgcmp  15008  cvgcmpce  15010  abscvgcvg  15011  isumsup2  15038  isumltss  15040  climcndslem1  15041  climcnds  15043  supcvg  15048  harmonic  15051  expcnv  15056  explecnv  15057  cvgrat  15076  mertenslem1  15077  mertenslem2  15078  clim2div  15082  ntrivcvgtail  15093  iprodclim2  15190  iprodclim3  15191  efcvg  15275  ege2le3  15280  efaddlem  15283  eftlub  15299  effsumlt  15301  tanhlt1  15350  ef01bndlem  15374  sin02gt0  15382  rpnnen2lem4  15407  ruclem2  15422  ruclem3  15423  ruclem9  15428  iddvdsexp  15470  dvdsadd  15489  dvdsfac  15513  dvdsmod  15515  3dvds  15517  omoe  15550  sumeven  15575  divalglem1  15582  flodddiv4t2lthalf  15604  bitsfzo  15621  bitsmod  15622  bitscmp  15624  bitsinv1lem  15627  sadcaddlem  15643  sadadd3  15647  sadaddlem  15652  dvdssqim  15737  dvdsmulgcd  15738  nn0seqcvgd  15747  dvdslcm  15775  lcmgcdlem  15783  dvdslcmf  15808  lcmfunsnlem2lem2  15816  mulgcddvds  15832  qredeq  15834  cncongr2  15845  sqnprm  15879  isprm6  15891  nonsq  15932  hashdvds  15945  prmdiv  15955  odzdvds  15965  pythagtriplem4  15989  pcpre1  16012  pcdvdsb  16038  pcz  16050  pcprmpw2  16051  pcaddlem  16057  pcadd  16058  pcadd2  16059  pcmpt  16061  pcmptdvds  16063  fldivp1  16066  pcfaclem  16067  pockthlem  16074  prmreclem1  16085  prmreclem3  16087  prmreclem5  16089  prmreclem6  16090  4sqlem6  16112  4sqlem8  16114  4sqlem11  16124  4sqlem12  16125  4sqlem14  16127  4sqlem16  16129  vdwlem3  16152  vdwlem9  16158  vdwlem10  16159  vdwlem12  16161  ramub1lem2  16196  prmgap  16228  prmgaplcm  16229  prmgapprmo  16231  mreexexd  16752  invfuc  17077  ple1  17487  eqgen  18090  lagsubg  18099  pgpfi  18464  sylow2alem2  18477  sylow2a  18478  sylow3lem4  18489  efgsrel  18591  odadd1  18695  odadd2  18696  gexex  18700  lt6abl  18740  dprd2d2  18887  dmdprdpr  18892  ablfacrp2  18910  ablfac1c  18914  pgpfaclem1  18924  ablfac2  18932  dvdsrmul1  19097  unitmulclb  19109  subrguss  19244  abvres  19304  ply1coefsupp  20150  evl1gsumadd  20207  znfld  20393  znunit  20396  frlmisfrlm  20678  matgsum  20734  pm2mpcl  21093  psmetxrge0  22610  isxmet2d  22624  mettri  22649  xmettri3  22650  mettri3  22651  xmetrtri2  22653  prdsxmetlem  22665  imasdsf1olem  22670  xblss2ps  22698  blss2ps  22700  blss2  22701  blssps  22721  blss  22722  prdsbl  22788  dscmet  22869  nmge0  22913  nmmtri  22918  tngngp3  22952  nlmvscnlem2  22981  nrginvrcnlem  22987  nmoix  23025  nmoleub  23027  blcvx  23093  xrsxmet  23104  opnreen  23126  xrge0tsms  23129  icopnfcnv  23233  xrhmeo  23237  lebnumii  23257  pcophtb  23320  pi1grplem  23340  nmoleub2lem  23405  ipcau2  23524  tcphcphlem1  23525  ipcau  23528  ipcnlem2  23534  rrxcph  23682  minveclem2  23716  minveclem3b  23718  pjthlem1  23727  pjthlem2  23728  ivthlem3  23741  ivth2  23743  ovolfsf  23759  ovolsslem  23772  ovollb2lem  23776  ovollb2  23777  ovolctb  23778  ovolfiniun  23789  ovolicc1  23804  ovolicc2lem4  23808  ovolicc2  23810  nulmbl2  23824  unmbl  23825  ioombl1lem4  23849  uniioombllem4  23874  uniioombllem6  23876  volivth  23895  vitalilem4  23899  itg1ge0  23974  itg1ge0a  23999  itg1lea  24000  itg1climres  24002  mbfi1fseqlem5  24007  itg2ub  24021  itg2seq  24030  itg2uba  24031  itg2splitlem  24036  itg2split  24037  itg2monolem3  24040  itg2mono  24041  itg2i1fseq2  24044  itg2addlem  24046  iblss  24092  itggt0  24129  dvferm2lem  24270  dvlip  24277  dvivthlem1  24292  dvfsumlem2  24311  dvfsumlem3  24312  ftc1lem4  24323  ply1divmo  24416  ply1remlem  24443  fta1glem2  24447  ig1pdvds  24457  plyeq0lem  24487  plydiveu  24574  fta1lem  24583  vieta1lem2  24587  aaliou3lem2  24619  aaliou3lem8  24621  ulmcn  24674  mtest  24679  itgulm  24683  radcnvlem1  24688  radcnvlt1  24693  dvradcnv  24696  pserdvlem2  24703  abelthlem2  24707  abelthlem6  24711  abelthlem7  24713  abelthlem9  24715  tangtx  24778  sinq12gt0  24780  sineq0  24796  cosordlem  24800  tanord  24807  tanregt0  24808  logrnaddcl  24843  logcj  24874  argregt0  24878  argrege0  24879  argimgt0  24880  argimlt0  24881  logimul  24882  logneg2  24883  logdivlti  24888  divlogrlim  24903  logcnlem3  24912  logcnlem4  24913  dvlog2lem  24920  logtayl  24928  rpcxpcl  24944  cxpsqrtlem  24970  cxpaddle  25018  isosctrlem1  25081  asinlem3a  25133  asinlem3  25134  asinneg  25149  asinsinlem  25154  asinsin  25155  atanlogaddlem  25176  atanlogadd  25177  atanlogsublem  25178  atanlogsub  25179  atantan  25186  atanbndlem  25188  atantayl  25200  leibpi  25206  birthdaylem3  25217  areaf  25225  cxploglim  25241  jensenlem2  25251  jensen  25252  logdiflbnd  25258  harmonicbnd4  25274  fsumharmonic  25275  zetacvg  25278  lgamgulmlem2  25293  lgamgulmlem3  25294  lgamcvg2  25318  wilthlem2  25332  wilthimp  25335  ftalem1  25336  ftalem2  25337  ftalem5  25340  basellem6  25349  basellem8  25351  basellem9  25352  chtge0  25375  chtublem  25473  logexprlim  25487  perfectlem1  25491  bcmax  25540  bposlem1  25546  bposlem2  25547  bposlem6  25551  bposlem7  25552  lgsdilem2  25595  lgsqrlem4  25611  lgsquadlem1  25642  2lgsoddprmlem2  25671  2sqlem3  25682  2sqlem8  25688  2sqblem  25693  2sqmod  25698  chebbnd1lem2  25732  chtppilimlem1  25735  chtppilim  25737  chto1ub  25738  vmadivsum  25744  rplogsumlem1  25746  rplogsumlem2  25747  dchrisum0lem1a  25748  rpvmasumlem  25749  dchrisumlem1  25751  dchrisumlem2  25752  dchrvmasumlem2  25760  dchrisum0flblem1  25770  dchrisum0flblem2  25771  dchrisum0lem1b  25777  dchrisum0lem1  25778  dchrisum0lem2a  25779  dchrisum0lem3  25781  dchrisum0  25782  mudivsum  25792  mulogsumlem  25793  mulog2sumlem1  25796  mulog2sumlem2  25797  2vmadivsumlem  25802  chpdifbndlem1  25815  selberg3lem1  25819  selberg4lem1  25822  pntrlog2bndlem1  25839  pntrlog2bndlem2  25840  pntrlog2bndlem3  25841  pntrlog2bndlem4  25842  pntpbnd1a  25847  pntpbnd1  25848  pntpbnd2  25849  pntibndlem2  25853  pntibndlem3  25854  pntlemd  25856  pntlemc  25857  pntlemb  25859  pntlemg  25860  pntlemh  25861  pntlemr  25864  pntlemf  25867  pntlemo  25869  abvcxp  25877  ostth2lem1  25880  padicabv  25892  ostth2lem2  25896  ostth2lem3  25897  ostth2lem4  25898  ostth2  25899  ostth3  25900  tgcgr4  26003  legso  26071  krippenlem  26162  midex  26209  oppperpex  26225  ttgcontlem1  26358  axpaschlem  26413  axcontlem8  26444  upgrex  26564  nbfusgrlevtxm1  26846  finsumvtxdgeven  27021  wwlksnextproplem3  27376  clwlkclwwlk2  27467  clwlkclwwlkfolem  27471  clwwlkndivn  27545  ex-ind-dvds  27928  nvabs  28136  nmooge0  28231  nmoolb  28235  siii  28317  minvecolem2  28339  minvecolem4  28344  minvecolem5  28345  hlipgt0  28378  normge0  28590  normpyc  28610  pjhthlem1  28855  pjige0i  29154  nmoplb  29371  nmfnlb  29388  branmfn  29569  pjssdif2i  29638  stlei  29704  xlt2addrd  30166  eliccelico  30184  elicoelioo  30185  bcm1n  30200  dvdszzq  30211  prmdvdsbc  30212  fsumiunle  30225  pfxlsw2ccat  30301  wrdt2ind  30302  omndmul2  30369  cyc3conja  30433  archirngz  30452  archiabllem2c  30458  xrge0tsmsd  30499  ofldchr  30537  fedgmullem2  30626  extdggt0  30647  psgnfzto1stlem  30660  madjusmdetlem2  30704  locfinreflem  30717  xrge0iifiso  30791  nexple  30881  gsumesum  30931  esumcst  30935  esumpcvgval  30950  esumcvg  30958  esumiun  30966  measssd  31087  measunl  31088  omssubadd  31171  carsgclctunlem3  31191  pmeasmono  31195  sibfof  31211  oddpwdc  31225  eulerpartlemgc  31233  iwrdsplit  31258  ballotlemsgt1  31381  ballotlemsel1i  31383  sgnmul  31413  signsply0  31434  signstfvc  31457  signsvtp  31466  signsvfpn  31468  fdvposlt  31483  fdvneggt  31484  fdvnegge  31486  logdivsqrle  31534  hgt750lemf  31537  tgoldbachgtde  31544  swrdwlk  31983  subfaclim  32045  erdszelem7  32054  erdszelem8  32055  cvmliftlem2  32143  snmlff  32186  sinccvglem  32525  climlec3  32575  faclim  32588  dvdspw  32592  nodense  32807  nosupbnd2lem1  32826  noetalem2  32829  fnejoin1  33327  poimirlem12  34456  poimirlem17  34461  poimirlem19  34463  poimirlem20  34464  poimirlem23  34467  poimirlem28  34472  broucube  34478  mblfinlem2  34482  mblfinlem3  34483  mblfinlem4  34484  ismblfin  34485  itg2addnclem  34495  itg2addnclem3  34497  itg2gt0cn  34499  itggt0cn  34516  ftc1anclem5  34523  ftc1anclem7  34525  ftc1anclem8  34526  isbnd3  34615  ssbnd  34619  heiborlem8  34649  bfplem2  34654  rrncmslem  34663  rrnequiv  34666  rrntotbnd  34667  lcv1  35729  lsatcv0eq  35735  lsatcvat3  35740  cvlsupr2  36031  hlatlej2  36064  cvrval4N  36102  cvratlem  36109  atcvr0eq  36114  2atlt  36127  atbtwnex  36136  athgt  36144  1cvrat  36164  ps-1  36165  hlatexch3N  36168  hlatexch4  36169  3atlem2  36172  atcvrlln2  36207  lplnexllnN  36252  4atlem3a  36285  4atlem10b  36293  4atlem11b  36296  4atlem12b  36299  2lplnja  36307  dalemply  36342  dalemsly  36343  dalem1  36347  dalem6  36356  dalem7  36357  dalem-cly  36359  dalem11  36362  dalem12  36363  dalem16  36367  dalem17  36368  dalem38  36398  dalem44  36404  dalem61  36421  lnatexN  36467  lncvrat  36470  lncmp  36471  paddasslem2  36509  dalawlem3  36561  dalawlem6  36564  dalawlem11  36569  lhpmcvr  36711  lhp2atne  36722  lhp2at0ne  36724  lautj  36781  trlval4  36876  cdlemc2  36880  cdlemc5  36883  cdleme3b  36917  cdleme11c  36949  cdleme19a  36991  cdleme20j  37006  cdleme22f  37034  cdleme23c  37039  cdleme26f2ALTN  37052  cdleme26f2  37053  cdleme35fnpq  37137  cdleme48bw  37190  cdlemg10a  37328  cdlemg11b  37330  cdlemg17g  37355  cdlemg18c  37368  cdlemi1  37506  cdlemk52  37642  dia2dimlem1  37752  dihord1  37906  dihjatcclem4  38109  cxpgt0d  38723  dvdsexpim  38724  fltnltalem  38792  fltnlta  38793  eldioph2lem1  38863  lzenom  38873  irrapxlem1  38925  irrapxlem4  38928  irrapxlem5  38929  pell14qrgt0  38962  pell1qrge1  38973  pell1qrgap  38977  pellfundge  38985  pellfundex  38989  pellfund14  39001  rmspecsqrtnq  39009  rmxypos  39050  ltrmynn0  39051  ltrmxnn0  39052  jm2.24nn  39062  jm2.17b  39064  jm2.17c  39065  jm2.24  39066  congadd  39069  congsym  39071  congneg  39072  congid  39074  mzpcong  39075  acongrep  39083  acongeq  39086  jm2.18  39091  jm2.19  39096  jm2.23  39099  jm2.25  39102  jm2.26lem3  39104  jm2.15nn0  39106  jm2.16nn0  39107  jm2.27a  39108  jm2.27c  39110  jm3.1lem1  39120  idomrootle  39301  idomsubgmo  39304  inductionexd  40011  imo72b2  40032  fincygsubgodd  40190  dvgrat  40203  radcnvrat  40205  binomcxplemnn0  40240  binomcxplemnotnn0  40247  cncmpmax  40849  rnmptlb  41076  zltlesub  41113  infxrpnf  41284  xrpnf  41325  fmul01  41424  fmul01lt1lem1  41428  climdivf  41456  sumnnodd  41474  climinf2lem  41550  limsup10exlem  41616  climliminf  41650  dfxlim2v  41691  xlimliminflimsup  41706  dvdivbd  41771  volge0  41809  stoweidlem1  41850  stoweidlem16  41865  stoweidlem18  41867  stoweidlem24  41873  stoweidlem26  41875  stoweidlem36  41885  stoweidlem38  41887  stoweidlem41  41890  stoweidlem42  41891  stoweidlem44  41893  stoweidlem45  41894  stoweidlem48  41897  stoweidlem62  41911  wallispilem5  41918  stirlinglem1  41923  stirlinglem5  41927  stirlinglem7  41929  stirlinglem8  41930  stirlinglem9  41931  stirlinglem11  41933  fourierdlem4  41960  fourierdlem10  41966  fourierdlem37  41993  fourierdlem47  42002  fourierdlem72  42027  fourierdlem74  42029  fourierdlem79  42034  fourierdlem82  42037  fourierdlem89  42044  fourierdlem91  42046  fourierdlem93  42048  fourierdlem103  42058  fourierdlem104  42059  fourierdlem112  42067  etransclem24  42107  etransclem25  42108  etransclem28  42111  etransclem37  42120  etransclem38  42121  etransclem44  42127  meaiuninc3v  42330  vonicclem1  42529  pimconstlt0  42546  smfsuplem1  42649  rlimdmafv  42914  rlimdmafv2  42995  2elfz2melfz  43056  iccpartgtprec  43084  iccpartlt  43088  iccpartgtl  43090  sqrtpwpw2p  43204  fmtnodvds  43210  goldbachthlem1  43211  lighneallem4a  43277  perfectALTVlem1  43390  cznnring  43727  rhmsubcrngc  43800  altgsumbcALT  43901  expnegico01  44076  flnn0div2ge  44096  rege1logbrege0  44121  fllogbd  44123  nnpw2blen  44143  nnolog2flm1  44153  dignn0ldlem  44165  dignn0flhalflem1  44178  dignn0flhalflem2  44179  eenglngeehlnmlem2  44228  itsclc0yqsol  44254  2itscp  44271  itscnhlinecirc02plem1  44272  itscnhlinecirc02plem2  44273  inlinecirc02p  44277