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  9647  onadju  10125  nnadju  10129  cfss  10196  tskuni  10714  ltexnq  10906  lt2addmuld  12410  div4p1lem1div2  12415  nn0le2x  12474  mul2lt0rgt0  13034  prodge0ld  13039  ge2halflem1  13046  xrmax1  13113  xrmax2  13114  max1ALT  13124  qbtwnxr  13138  xleadd1a  13191  xlt2add  13198  xlesubadd  13201  xmulgt0  13221  xlemul1a  13226  xov1plusxeqvd  13437  uzsubsubfz  13485  fzctr  13579  subfzo0  13728  flflp1  13747  fldiv4lem1div2uz2  13776  ceilge  13785  modge0  13819  modlt  13820  modid  13836  m1modge3gt1  13861  modaddmodup  13877  sermono  13977  seqf1olem1  13984  seqf1olem2  13985  sqgt0  14069  sqge0  14079  leexp1a  14118  nnlesq  14148  expnbnd  14175  expmulnbnd  14178  discr1  14182  facwordi  14232  faclbnd5  14241  nfile  14302  hashdom  14322  hashgt23el  14367  fi1uzind  14450  brfi1indALT  14453  ccatws1n0  14575  swrds2  14883  cjmulge0  15089  resqrtcl  15196  absge0  15230  sqreulem  15303  amgm2  15313  rlimdm  15494  rlimge0  15524  reccn2  15540  climle  15583  climserle  15606  isercoll2  15612  iseraltlem1  15625  iseralt  15628  isumclim2  15701  isumclim3  15702  isumge0  15709  fsumless  15739  cvgcmp  15759  cvgcmpce  15761  abscvgcvg  15762  isumsup2  15789  isumltss  15791  climcndslem1  15792  climcnds  15794  supcvg  15799  harmonic  15802  expcnv  15807  explecnv  15808  cvgrat  15826  mertenslem1  15827  mertenslem2  15828  clim2div  15832  ntrivcvgtail  15843  iprodclim2  15942  iprodclim3  15943  efcvg  16028  ege2le3  16033  efaddlem  16036  eftlub  16054  effsumlt  16056  tanhlt1  16105  ef01bndlem  16129  sin02gt0  16137  rpnnen2lem4  16162  ruclem2  16177  ruclem3  16178  ruclem9  16183  iddvdsexp  16226  dvdsadd  16249  dvdsfac  16273  dvdsexp2im  16274  dvdsmod  16276  3dvds  16278  omoe  16311  sumeven  16334  divalglem1  16341  flodddiv4t2lthalf  16365  bitsfzo  16382  bitsmod  16383  bitscmp  16385  bitsinv1lem  16388  sadcaddlem  16404  sadadd3  16408  sadaddlem  16413  dvdssqim  16501  dvdsexpim  16502  dvdsmulgcd  16503  nn0seqcvgd  16517  dvdslcm  16545  lcmgcdlem  16553  dvdslcmf  16578  lcmfunsnlem2lem2  16586  mulgcddvds  16602  qredeq  16604  cncongr2  16615  sqnprm  16649  isprm6  16661  dvdszzq  16668  prmdvdsbc  16673  nonsq  16706  hashdvds  16722  prmdiv  16732  odzdvds  16743  pythagtriplem4  16767  pcpre1  16790  pcdvdsb  16817  pcz  16829  pcprmpw2  16830  pcaddlem  16836  pcadd  16837  pcadd2  16838  pcmpt  16840  pcmptdvds  16842  fldivp1  16845  pcfaclem  16846  pockthlem  16853  prmreclem1  16864  prmreclem3  16866  prmreclem5  16868  prmreclem6  16869  4sqlem6  16891  4sqlem8  16893  4sqlem11  16903  4sqlem12  16904  4sqlem14  16906  4sqlem16  16908  vdwlem3  16931  vdwlem9  16937  vdwlem10  16938  vdwlem12  16940  ramub1lem2  16975  prmgap  17007  prmgaplcm  17008  prmgapprmo  17010  mreexexd  17590  invfuc  17920  ple1  18370  eqgen  19096  lagsubg  19110  pgpfi  19520  sylow2alem2  19533  sylow2a  19534  sylow3lem4  19545  efgsrel  19649  odadd1  19763  odadd2  19764  gexex  19768  lt6abl  19810  dprd2d2  19961  dmdprdpr  19966  ablfacrp2  19984  ablfac1c  19988  pgpfaclem1  19998  ablfac2  20006  fincygsubgodd  20029  omndmul2  20048  dvdsrmul1  20290  unitmulclb  20302  subrguss  20508  rhmsubcrngc  20589  abvres  20752  znfld  21503  znunit  21506  ofldchr  21519  frlmisfrlm  21791  ply1coefsupp  22218  evl1gsumadd  22279  matgsum  22358  pm2mpcl  22718  psmetxrge0  24235  isxmet2d  24249  mettri  24274  xmettri3  24275  mettri3  24276  xmetrtri2  24278  prdsxmetlem  24290  imasdsf1olem  24295  xblss2ps  24323  blss2ps  24325  blss2  24326  blssps  24346  blss  24347  prdsbl  24413  dscmet  24494  nmge0  24539  nmmtri  24544  tngngp3  24578  nlmvscnlem2  24607  nrginvrcnlem  24613  nmoix  24651  nmoleub  24653  blcvx  24720  xrsxmet  24732  opnreen  24754  xrge0tsms  24757  icopnfcnv  24874  xrhmeo  24878  lebnumii  24899  pcophtb  24963  pi1grplem  24983  nmoleub2lem  25048  ipcau2  25168  tcphcphlem1  25169  ipcau  25172  ipcnlem2  25178  rrxcph  25326  minveclem2  25360  minveclem3b  25362  pjthlem1  25371  pjthlem2  25372  ivthlem3  25388  ivth2  25390  ovolfsf  25406  ovolsslem  25419  ovollb2lem  25423  ovollb2  25424  ovolctb  25425  ovolfiniun  25436  ovolicc1  25451  ovolicc2lem4  25455  ovolicc2  25457  nulmbl2  25471  unmbl  25472  ioombl1lem4  25496  uniioombllem4  25521  uniioombllem6  25523  volivth  25542  vitalilem4  25546  itg1ge0  25621  itg1ge0a  25646  itg1lea  25647  itg1climres  25649  mbfi1fseqlem5  25654  itg2ub  25668  itg2seq  25677  itg2uba  25678  itg2splitlem  25683  itg2split  25684  itg2monolem3  25687  itg2mono  25688  itg2i1fseq2  25691  itg2addlem  25693  iblss  25740  itggt0  25779  dvferm2lem  25924  dvlip  25932  dvivthlem1  25947  dvfsumlem2  25967  dvfsumlem2OLD  25968  dvfsumlem3  25969  ftc1lem4  25980  ply1divmo  26075  ply1remlem  26104  fta1glem2  26108  idomrootle  26112  ig1pdvds  26119  plyeq0lem  26149  plydiveu  26240  fta1lem  26249  vieta1lem2  26253  aaliou3lem2  26285  aaliou3lem8  26287  ulmcn  26342  mtest  26347  itgulm  26351  radcnvlem1  26356  radcnvlt1  26361  dvradcnv  26364  pserdvlem2  26372  abelthlem2  26376  abelthlem6  26380  abelthlem7  26382  abelthlem9  26384  tangtx  26448  sinq12gt0  26450  sineq0  26467  cosordlem  26473  tanord  26481  tanregt0  26482  logrnaddcl  26517  logcj  26549  argregt0  26553  argrege0  26554  argimgt0  26555  argimlt0  26556  logimul  26557  logneg2  26558  logdivlti  26563  divlogrlim  26578  logcnlem3  26587  logcnlem4  26588  dvlog2lem  26595  logtayl  26603  rpcxpcl  26619  cxpsqrtlem  26645  cxpaddle  26696  isosctrlem1  26762  asinlem3a  26814  asinlem3  26815  asinneg  26830  asinsinlem  26835  asinsin  26836  atanlogaddlem  26857  atanlogadd  26858  atanlogsublem  26859  atanlogsub  26860  atantan  26867  atanbndlem  26869  atantayl  26881  leibpi  26886  birthdaylem3  26897  areaf  26905  cxploglim  26922  jensenlem2  26932  jensen  26933  logdiflbnd  26939  harmonicbnd4  26955  fsumharmonic  26956  zetacvg  26959  lgamgulmlem2  26974  lgamgulmlem3  26975  lgamcvg2  26999  wilthlem2  27013  wilthimp  27016  ftalem1  27017  ftalem2  27018  ftalem5  27021  basellem6  27030  basellem8  27032  basellem9  27033  chtge0  27056  chtublem  27156  logexprlim  27170  perfectlem1  27174  bcmax  27223  bposlem1  27229  bposlem2  27230  bposlem6  27234  bposlem7  27235  lgsdilem2  27278  lgsqrlem4  27294  lgsquadlem1  27325  2lgsoddprmlem2  27354  2sqlem3  27365  2sqlem8  27371  2sqblem  27376  2sqmod  27381  chebbnd1lem2  27415  chtppilimlem1  27418  chtppilim  27420  chto1ub  27421  vmadivsum  27427  rplogsumlem1  27429  rplogsumlem2  27430  dchrisum0lem1a  27431  rpvmasumlem  27432  dchrisumlem1  27434  dchrisumlem2  27435  dchrvmasumlem2  27443  dchrisum0flblem1  27453  dchrisum0flblem2  27454  dchrisum0lem1b  27460  dchrisum0lem1  27461  dchrisum0lem2a  27462  dchrisum0lem3  27464  dchrisum0  27465  mudivsum  27475  mulogsumlem  27476  mulog2sumlem1  27479  mulog2sumlem2  27480  2vmadivsumlem  27485  chpdifbndlem1  27498  selberg3lem1  27502  selberg4lem1  27505  pntrlog2bndlem1  27522  pntrlog2bndlem2  27523  pntrlog2bndlem3  27524  pntrlog2bndlem4  27525  pntpbnd1a  27530  pntpbnd1  27531  pntpbnd2  27532  pntibndlem2  27536  pntibndlem3  27537  pntlemd  27539  pntlemc  27540  pntlemb  27542  pntlemg  27543  pntlemh  27544  pntlemr  27547  pntlemf  27550  pntlemo  27552  abvcxp  27560  ostth2lem1  27563  padicabv  27575  ostth2lem2  27579  ostth2lem3  27580  ostth2lem4  27581  ostth2  27582  ostth3  27583  nodense  27638  nogt01o  27642  nosupbnd2lem1  27661  noetasuplem3  27681  maxs1  27711  maxs2  27712  eqscut3  27771  cofcutr  27873  cofcutrtime  27876  addsuniflem  27949  negsunif  28002  ssltmul2  28092  precsexlem11  28160  abssge0  28188  sleabs  28191  onscutlt  28206  om2noseqlt  28234  zsoring  28337  expsgt0  28365  halfcut  28382  addhalfcut  28383  tgcgr4  28512  legso  28580  krippenlem  28671  midex  28718  oppperpex  28734  ttgcontlem1  28866  axpaschlem  28921  axcontlem8  28952  upgrex  29073  nbfusgrlevtxm1  29358  finsumvtxdgeven  29534  wwlksnextproplem3  29892  clwlkclwwlk2  29983  clwlkclwwlkfolem  29987  clwwlkndivn  30060  ex-ind-dvds  30441  nvabs  30652  nmooge0  30747  nmoolb  30751  siii  30833  minvecolem2  30855  minvecolem4  30860  minvecolem5  30861  hlipgt0  30894  normge0  31106  normpyc  31126  pjhthlem1  31371  pjige0i  31670  nmoplb  31887  nmfnlb  31904  branmfn  32085  pjssdif2i  32154  stlei  32220  xlt2addrd  32733  eliccelico  32751  elicoelioo  32752  bcm1n  32769  fsumiunle  32805  sgnmul  32811  nexple  32820  expevenpos  32822  ccatdmss  32922  pfxlsw2ccat  32923  wrdt2ind  32926  chnub  32985  xrge0tsmsd  33046  gsumwrd2dccatlem  33050  psgnfzto1stlem  33073  cycpmco2lem4  33102  cycpmco2lem5  33103  cyc3conja  33130  archirngz  33159  archiabllem2c  33165  rprmasso2  33491  rprmirred  33496  1arithufdlem3  33511  lbslelsp  33587  fedgmullem2  33620  extdggt0  33647  evls1fldgencl  33659  fldextrspunlem1  33664  algextdeglem8  33708  rtelextdg2lem  33710  cos9thpiminplylem1  33766  cos9thpiminplylem2  33767  madjusmdetlem2  33812  locfinreflem  33824  xrge0iifiso  33919  gsumesum  34043  esumcst  34047  esumpcvgval  34062  esumcvg  34070  esumiun  34078  measssd  34199  measunl  34200  omssubadd  34285  carsgclctunlem3  34305  pmeasmono  34309  sibfof  34325  oddpwdc  34339  eulerpartlemgc  34347  iwrdsplit  34372  ballotlemsgt1  34496  ballotlemsel1i  34498  signsply0  34536  signstfvc  34559  signsvtp  34568  signsvfpn  34570  fdvposlt  34584  fdvneggt  34585  fdvnegge  34587  logdivsqrle  34635  hgt750lemf  34638  tgoldbachgtde  34645  swrdwlk  35108  subfaclim  35169  erdszelem7  35178  erdszelem8  35179  cvmliftlem2  35267  snmlff  35310  sinccvglem  35653  climlec3  35715  faclim  35727  fnejoin1  36350  poimirlem12  37620  poimirlem17  37625  poimirlem19  37627  poimirlem20  37628  poimirlem23  37631  poimirlem28  37636  broucube  37642  mblfinlem2  37646  mblfinlem3  37647  mblfinlem4  37648  ismblfin  37649  itg2addnclem  37659  itg2addnclem3  37661  itg2gt0cn  37663  itggt0cn  37678  ftc1anclem5  37685  ftc1anclem7  37687  ftc1anclem8  37688  isbnd3  37772  ssbnd  37776  heiborlem8  37806  bfplem2  37811  rrncmslem  37820  rrnequiv  37823  rrntotbnd  37824  lcv1  39028  lsatcv0eq  39034  lsatcvat3  39039  cvlsupr2  39330  hlatlej2  39363  cvrval4N  39402  cvratlem  39409  atcvr0eq  39414  2atlt  39427  atbtwnex  39436  athgt  39444  1cvrat  39464  ps-1  39465  hlatexch3N  39468  hlatexch4  39469  3atlem2  39472  atcvrlln2  39507  lplnexllnN  39552  4atlem3a  39585  4atlem10b  39593  4atlem11b  39596  4atlem12b  39599  2lplnja  39607  dalemply  39642  dalemsly  39643  dalem1  39647  dalem6  39656  dalem7  39657  dalem-cly  39659  dalem11  39662  dalem12  39663  dalem16  39667  dalem17  39668  dalem38  39698  dalem44  39704  dalem61  39721  lnatexN  39767  lncvrat  39770  lncmp  39771  paddasslem2  39809  dalawlem3  39861  dalawlem6  39864  dalawlem11  39869  lhpmcvr  40011  lhp2atne  40022  lhp2at0ne  40024  lautj  40081  trlval4  40176  cdlemc2  40180  cdlemc5  40183  cdleme3b  40217  cdleme11c  40249  cdleme19a  40291  cdleme20j  40306  cdleme22f  40334  cdleme23c  40339  cdleme26f2ALTN  40352  cdleme26f2  40353  cdleme35fnpq  40437  cdleme48bw  40490  cdlemg10a  40628  cdlemg11b  40630  cdlemg17g  40655  cdlemg18c  40668  cdlemi1  40806  cdlemk52  40942  dia2dimlem1  41052  dihord1  41206  dihjatcclem4  41409  lcmineqlem15  42025  lcmineqlem19  42029  lcmineqlem22  42032  aks4d1lem1  42044  aks4d1p1p4  42053  aks4d1p1p5  42057  aks4d1p2  42059  aks4d1p3  42060  aks4d1p6  42063  aks4d1p7d1  42064  aks4d1p7  42065  aks4d1p8  42069  aks4d1p9  42070  aks6d1c1p6  42096  aks6d1c1  42098  aks6d1c2  42112  sticksstones7  42134  aks6d1c7lem1  42162  unitscyglem4  42180  dvdsexpnn0  42316  prjspner01  42607  flt4lem5  42632  fltnltalem  42644  fltnlta  42645  3cubeslem1  42666  eldioph2lem1  42742  lzenom  42752  irrapxlem1  42804  irrapxlem4  42807  irrapxlem5  42808  pell14qrgt0  42841  pell1qrge1  42852  pell1qrgap  42856  pellfundge  42864  pellfundex  42868  pellfund14  42880  rmspecsqrtnq  42888  rmxypos  42930  ltrmynn0  42931  ltrmxnn0  42932  jm2.24nn  42942  jm2.17b  42944  jm2.17c  42945  jm2.24  42946  congadd  42949  congsym  42951  congneg  42952  congid  42954  mzpcong  42955  acongrep  42963  acongeq  42966  jm2.18  42971  jm2.19  42976  jm2.23  42979  jm2.25  42982  jm2.26lem3  42984  jm2.15nn0  42986  jm2.16nn0  42987  jm2.27a  42988  jm2.27c  42990  jm3.1lem1  43000  idomsubgmo  43176  sqrtcval  43624  inductionexd  44138  imo72b2lem0  44148  imo72b2  44155  dvgrat  44295  radcnvrat  44297  binomcxplemnn0  44332  binomcxplemnotnn0  44339  cncmpmax  45020  rnmptlb  45231  zltlesub  45277  infxrpnf  45436  xrpnf  45475  fmul01  45572  fmul01lt1lem1  45576  climdivf  45604  sumnnodd  45622  climinf2lem  45698  limsup10exlem  45764  climliminf  45798  dfxlim2v  45839  xlimliminflimsup  45854  dvdivbd  45915  volge0  45953  stoweidlem1  45993  stoweidlem16  46008  stoweidlem18  46010  stoweidlem24  46016  stoweidlem26  46018  stoweidlem36  46028  stoweidlem38  46030  stoweidlem41  46033  stoweidlem42  46034  stoweidlem44  46036  stoweidlem45  46037  stoweidlem48  46040  stoweidlem62  46054  wallispilem5  46061  stirlinglem1  46066  stirlinglem5  46070  stirlinglem7  46072  stirlinglem8  46073  stirlinglem9  46074  stirlinglem11  46076  fourierdlem4  46103  fourierdlem10  46109  fourierdlem37  46136  fourierdlem47  46145  fourierdlem72  46170  fourierdlem74  46172  fourierdlem79  46177  fourierdlem82  46180  fourierdlem89  46187  fourierdlem91  46189  fourierdlem93  46191  fourierdlem103  46201  fourierdlem104  46202  fourierdlem112  46210  etransclem24  46250  etransclem25  46251  etransclem28  46254  etransclem37  46263  etransclem38  46264  etransclem44  46270  meaiuninc3v  46476  vonicclem1  46675  pimconstlt0  46693  smfsuplem1  46803  rlimdmafv  47172  rlimdmafv2  47253  2elfz2melfz  47313  iccpartgtprec  47415  iccpartlt  47419  iccpartgtl  47421  sqrtpwpw2p  47533  fmtnodvds  47539  goldbachthlem1  47540  lighneallem4a  47603  perfectALTVlem1  47716  uhgrimgrlim  47980  cznnring  48244  altgsumbcALT  48335  expnegico01  48501  flnn0div2ge  48516  rege1logbrege0  48541  fllogbd  48543  nnpw2blen  48563  nnolog2flm1  48573  dignn0ldlem  48585  dignn0flhalflem1  48598  dignn0flhalflem2  48599  eenglngeehlnmlem2  48721  itsclc0yqsol  48747  2itscp  48764  itscnhlinecirc02plem1  48765  itscnhlinecirc02plem2  48766  inlinecirc02p  48770