Theorem breqtrrd 5120

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 5118	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  marypha1lem  9323  marypha2  9329  infsupprpr  9396  unxpwdom  9481  ttrcltr  9612  onadju  10088  nnadju  10092  cfss  10159  tskuni  10677  ltexnq  10869  lt2addmuld  12374  div4p1lem1div2  12379  nn0le2x  12438  mul2lt0rgt0  12998  prodge0ld  13003  ge2halflem1  13010  xrmax1  13077  xrmax2  13078  max1ALT  13088  qbtwnxr  13102  xleadd1a  13155  xlt2add  13162  xlesubadd  13165  xmulgt0  13185  xlemul1a  13190  xov1plusxeqvd  13401  uzsubsubfz  13449  fzctr  13543  subfzo0  13692  flflp1  13711  fldiv4lem1div2uz2  13740  ceilge  13749  modge0  13783  modlt  13784  modid  13800  m1modge3gt1  13825  modaddmodup  13841  sermono  13941  seqf1olem1  13948  seqf1olem2  13949  sqgt0  14033  sqge0  14043  leexp1a  14082  nnlesq  14112  expnbnd  14139  expmulnbnd  14142  discr1  14146  facwordi  14196  faclbnd5  14205  nfile  14266  hashdom  14286  hashgt23el  14331  fi1uzind  14414  brfi1indALT  14417  ccatws1n0  14539  swrds2  14847  cjmulge0  15053  resqrtcl  15160  absge0  15194  sqreulem  15267  amgm2  15277  rlimdm  15458  rlimge0  15488  reccn2  15504  climle  15547  climserle  15570  isercoll2  15576  iseraltlem1  15589  iseralt  15592  isumclim2  15665  isumclim3  15666  isumge0  15673  fsumless  15703  cvgcmp  15723  cvgcmpce  15725  abscvgcvg  15726  isumsup2  15753  isumltss  15755  climcndslem1  15756  climcnds  15758  supcvg  15763  harmonic  15766  expcnv  15771  explecnv  15772  cvgrat  15790  mertenslem1  15791  mertenslem2  15792  clim2div  15796  ntrivcvgtail  15807  iprodclim2  15906  iprodclim3  15907  efcvg  15992  ege2le3  15997  efaddlem  16000  eftlub  16018  effsumlt  16020  tanhlt1  16069  ef01bndlem  16093  sin02gt0  16101  rpnnen2lem4  16126  ruclem2  16141  ruclem3  16142  ruclem9  16147  iddvdsexp  16190  dvdsadd  16213  dvdsfac  16237  dvdsexp2im  16238  dvdsmod  16240  3dvds  16242  omoe  16275  sumeven  16298  divalglem1  16305  flodddiv4t2lthalf  16329  bitsfzo  16346  bitsmod  16347  bitscmp  16349  bitsinv1lem  16352  sadcaddlem  16368  sadadd3  16372  sadaddlem  16377  dvdssqim  16465  dvdsexpim  16466  dvdsmulgcd  16467  nn0seqcvgd  16481  dvdslcm  16509  lcmgcdlem  16517  dvdslcmf  16542  lcmfunsnlem2lem2  16550  mulgcddvds  16566  qredeq  16568  cncongr2  16579  sqnprm  16613  isprm6  16625  dvdszzq  16632  prmdvdsbc  16637  nonsq  16670  hashdvds  16686  prmdiv  16696  odzdvds  16707  pythagtriplem4  16731  pcpre1  16754  pcdvdsb  16781  pcz  16793  pcprmpw2  16794  pcaddlem  16800  pcadd  16801  pcadd2  16802  pcmpt  16804  pcmptdvds  16806  fldivp1  16809  pcfaclem  16810  pockthlem  16817  prmreclem1  16828  prmreclem3  16830  prmreclem5  16832  prmreclem6  16833  4sqlem6  16855  4sqlem8  16857  4sqlem11  16867  4sqlem12  16868  4sqlem14  16870  4sqlem16  16872  vdwlem3  16895  vdwlem9  16901  vdwlem10  16902  vdwlem12  16904  ramub1lem2  16939  prmgap  16971  prmgaplcm  16972  prmgapprmo  16974  mreexexd  17554  invfuc  17884  ple1  18334  eqgen  19060  lagsubg  19074  pgpfi  19484  sylow2alem2  19497  sylow2a  19498  sylow3lem4  19509  efgsrel  19613  odadd1  19727  odadd2  19728  gexex  19732  lt6abl  19774  dprd2d2  19925  dmdprdpr  19930  ablfacrp2  19948  ablfac1c  19952  pgpfaclem1  19962  ablfac2  19970  fincygsubgodd  19993  omndmul2  20012  dvdsrmul1  20254  unitmulclb  20266  subrguss  20472  rhmsubcrngc  20553  abvres  20716  znfld  21467  znunit  21470  ofldchr  21483  frlmisfrlm  21755  ply1coefsupp  22182  evl1gsumadd  22243  matgsum  22322  pm2mpcl  22682  psmetxrge0  24199  isxmet2d  24213  mettri  24238  xmettri3  24239  mettri3  24240  xmetrtri2  24242  prdsxmetlem  24254  imasdsf1olem  24259  xblss2ps  24287  blss2ps  24289  blss2  24290  blssps  24310  blss  24311  prdsbl  24377  dscmet  24458  nmge0  24503  nmmtri  24508  tngngp3  24542  nlmvscnlem2  24571  nrginvrcnlem  24577  nmoix  24615  nmoleub  24617  blcvx  24684  xrsxmet  24696  opnreen  24718  xrge0tsms  24721  icopnfcnv  24838  xrhmeo  24842  lebnumii  24863  pcophtb  24927  pi1grplem  24947  nmoleub2lem  25012  ipcau2  25132  tcphcphlem1  25133  ipcau  25136  ipcnlem2  25142  rrxcph  25290  minveclem2  25324  minveclem3b  25326  pjthlem1  25335  pjthlem2  25336  ivthlem3  25352  ivth2  25354  ovolfsf  25370  ovolsslem  25383  ovollb2lem  25387  ovollb2  25388  ovolctb  25389  ovolfiniun  25400  ovolicc1  25415  ovolicc2lem4  25419  ovolicc2  25421  nulmbl2  25435  unmbl  25436  ioombl1lem4  25460  uniioombllem4  25485  uniioombllem6  25487  volivth  25506  vitalilem4  25510  itg1ge0  25585  itg1ge0a  25610  itg1lea  25611  itg1climres  25613  mbfi1fseqlem5  25618  itg2ub  25632  itg2seq  25641  itg2uba  25642  itg2splitlem  25647  itg2split  25648  itg2monolem3  25651  itg2mono  25652  itg2i1fseq2  25655  itg2addlem  25657  iblss  25704  itggt0  25743  dvferm2lem  25888  dvlip  25896  dvivthlem1  25911  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  ftc1lem4  25944  ply1divmo  26039  ply1remlem  26068  fta1glem2  26072  idomrootle  26076  ig1pdvds  26083  plyeq0lem  26113  plydiveu  26204  fta1lem  26213  vieta1lem2  26217  aaliou3lem2  26249  aaliou3lem8  26251  ulmcn  26306  mtest  26311  itgulm  26315  radcnvlem1  26320  radcnvlt1  26325  dvradcnv  26328  pserdvlem2  26336  abelthlem2  26340  abelthlem6  26344  abelthlem7  26346  abelthlem9  26348  tangtx  26412  sinq12gt0  26414  sineq0  26431  cosordlem  26437  tanord  26445  tanregt0  26446  logrnaddcl  26481  logcj  26513  argregt0  26517  argrege0  26518  argimgt0  26519  argimlt0  26520  logimul  26521  logneg2  26522  logdivlti  26527  divlogrlim  26542  logcnlem3  26551  logcnlem4  26552  dvlog2lem  26559  logtayl  26567  rpcxpcl  26583  cxpsqrtlem  26609  cxpaddle  26660  isosctrlem1  26726  asinlem3a  26778  asinlem3  26779  asinneg  26794  asinsinlem  26799  asinsin  26800  atanlogaddlem  26821  atanlogadd  26822  atanlogsublem  26823  atanlogsub  26824  atantan  26831  atanbndlem  26833  atantayl  26845  leibpi  26850  birthdaylem3  26861  areaf  26869  cxploglim  26886  jensenlem2  26896  jensen  26897  logdiflbnd  26903  harmonicbnd4  26919  fsumharmonic  26920  zetacvg  26923  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamcvg2  26963  wilthlem2  26977  wilthimp  26980  ftalem1  26981  ftalem2  26982  ftalem5  26985  basellem6  26994  basellem8  26996  basellem9  26997  chtge0  27020  chtublem  27120  logexprlim  27134  perfectlem1  27138  bcmax  27187  bposlem1  27193  bposlem2  27194  bposlem6  27198  bposlem7  27199  lgsdilem2  27242  lgsqrlem4  27258  lgsquadlem1  27289  2lgsoddprmlem2  27318  2sqlem3  27329  2sqlem8  27335  2sqblem  27340  2sqmod  27345  chebbnd1lem2  27379  chtppilimlem1  27382  chtppilim  27384  chto1ub  27385  vmadivsum  27391  rplogsumlem1  27393  rplogsumlem2  27394  dchrisum0lem1a  27395  rpvmasumlem  27396  dchrisumlem1  27398  dchrisumlem2  27399  dchrvmasumlem2  27407  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem3  27428  dchrisum0  27429  mudivsum  27439  mulogsumlem  27440  mulog2sumlem1  27443  mulog2sumlem2  27444  2vmadivsumlem  27449  chpdifbndlem1  27462  selberg3lem1  27466  selberg4lem1  27469  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem2  27500  pntibndlem3  27501  pntlemd  27503  pntlemc  27504  pntlemb  27506  pntlemg  27507  pntlemh  27508  pntlemr  27511  pntlemf  27514  pntlemo  27516  abvcxp  27524  ostth2lem1  27527  padicabv  27539  ostth2lem2  27543  ostth2lem3  27544  ostth2lem4  27545  ostth2  27546  ostth3  27547  nodense  27602  nogt01o  27606  nosupbnd2lem1  27625  noetasuplem3  27645  maxs1  27675  maxs2  27676  eqscut3  27736  cofcutr  27839  cofcutrtime  27842  addsuniflem  27915  negsunif  27968  ssltmul2  28058  precsexlem11  28126  abssge0  28154  sleabs  28157  onscutlt  28172  om2noseqlt  28200  zsoring  28303  expsgt0  28331  halfcut  28349  addhalfcut  28350  tgcgr4  28480  legso  28548  krippenlem  28639  midex  28686  oppperpex  28702  ttgcontlem1  28834  axpaschlem  28889  axcontlem8  28920  upgrex  29041  nbfusgrlevtxm1  29326  finsumvtxdgeven  29502  wwlksnextproplem3  29860  clwlkclwwlk2  29951  clwlkclwwlkfolem  29955  clwwlkndivn  30028  ex-ind-dvds  30409  nvabs  30620  nmooge0  30715  nmoolb  30719  siii  30801  minvecolem2  30823  minvecolem4  30828  minvecolem5  30829  hlipgt0  30862  normge0  31074  normpyc  31094  pjhthlem1  31339  pjige0i  31638  nmoplb  31855  nmfnlb  31872  branmfn  32053  pjssdif2i  32122  stlei  32188  xlt2addrd  32711  eliccelico  32729  elicoelioo  32730  bcm1n  32747  fsumiunle  32783  sgnmul  32789  nexple  32798  expevenpos  32800  ccatdmss  32900  pfxlsw2ccat  32901  wrdt2ind  32904  chnub  32963  xrge0tsmsd  33024  gsumwrd2dccatlem  33028  psgnfzto1stlem  33051  cycpmco2lem4  33080  cycpmco2lem5  33081  cyc3conja  33108  archirngz  33140  archiabllem2c  33146  rprmasso2  33472  rprmirred  33477  1arithufdlem3  33492  lbslelsp  33580  fedgmullem2  33613  extdggt0  33640  evls1fldgencl  33653  fldextrspunlem1  33658  extdgfialglem1  33675  algextdeglem8  33707  rtelextdg2lem  33709  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  madjusmdetlem2  33811  locfinreflem  33823  xrge0iifiso  33918  gsumesum  34042  esumcst  34046  esumpcvgval  34061  esumcvg  34069  esumiun  34077  measssd  34198  measunl  34199  omssubadd  34284  carsgclctunlem3  34304  pmeasmono  34308  sibfof  34324  oddpwdc  34338  eulerpartlemgc  34346  iwrdsplit  34371  ballotlemsgt1  34495  ballotlemsel1i  34497  signsply0  34535  signstfvc  34558  signsvtp  34567  signsvfpn  34569  fdvposlt  34583  fdvneggt  34584  fdvnegge  34586  logdivsqrle  34634  hgt750lemf  34637  tgoldbachgtde  34644  swrdwlk  35120  subfaclim  35181  erdszelem7  35190  erdszelem8  35191  cvmliftlem2  35279  snmlff  35322  sinccvglem  35665  climlec3  35727  faclim  35739  fnejoin1  36362  poimirlem12  37632  poimirlem17  37637  poimirlem19  37639  poimirlem20  37640  poimirlem23  37643  poimirlem28  37648  broucube  37654  mblfinlem2  37658  mblfinlem3  37659  mblfinlem4  37660  ismblfin  37661  itg2addnclem  37671  itg2addnclem3  37673  itg2gt0cn  37675  itggt0cn  37690  ftc1anclem5  37697  ftc1anclem7  37699  ftc1anclem8  37700  isbnd3  37784  ssbnd  37788  heiborlem8  37818  bfplem2  37823  rrncmslem  37832  rrnequiv  37835  rrntotbnd  37836  lcv1  39040  lsatcv0eq  39046  lsatcvat3  39051  cvlsupr2  39342  hlatlej2  39375  cvrval4N  39413  cvratlem  39420  atcvr0eq  39425  2atlt  39438  atbtwnex  39447  athgt  39455  1cvrat  39475  ps-1  39476  hlatexch3N  39479  hlatexch4  39480  3atlem2  39483  atcvrlln2  39518  lplnexllnN  39563  4atlem3a  39596  4atlem10b  39604  4atlem11b  39607  4atlem12b  39610  2lplnja  39618  dalemply  39653  dalemsly  39654  dalem1  39658  dalem6  39667  dalem7  39668  dalem-cly  39670  dalem11  39673  dalem12  39674  dalem16  39678  dalem17  39679  dalem38  39709  dalem44  39715  dalem61  39732  lnatexN  39778  lncvrat  39781  lncmp  39782  paddasslem2  39820  dalawlem3  39872  dalawlem6  39875  dalawlem11  39880  lhpmcvr  40022  lhp2atne  40033  lhp2at0ne  40035  lautj  40092  trlval4  40187  cdlemc2  40191  cdlemc5  40194  cdleme3b  40228  cdleme11c  40260  cdleme19a  40302  cdleme20j  40317  cdleme22f  40345  cdleme23c  40350  cdleme26f2ALTN  40363  cdleme26f2  40364  cdleme35fnpq  40448  cdleme48bw  40501  cdlemg10a  40639  cdlemg11b  40641  cdlemg17g  40666  cdlemg18c  40679  cdlemi1  40817  cdlemk52  40953  dia2dimlem1  41063  dihord1  41217  dihjatcclem4  41420  lcmineqlem15  42036  lcmineqlem19  42040  lcmineqlem22  42043  aks4d1lem1  42055  aks4d1p1p4  42064  aks4d1p1p5  42068  aks4d1p2  42070  aks4d1p3  42071  aks4d1p6  42074  aks4d1p7d1  42075  aks4d1p7  42076  aks4d1p8  42080  aks4d1p9  42081  aks6d1c1p6  42107  aks6d1c1  42109  aks6d1c2  42123  sticksstones7  42145  aks6d1c7lem1  42173  unitscyglem4  42191  dvdsexpnn0  42327  prjspner01  42618  flt4lem5  42643  fltnltalem  42655  fltnlta  42656  3cubeslem1  42677  eldioph2lem1  42753  lzenom  42763  irrapxlem1  42815  irrapxlem4  42818  irrapxlem5  42819  pell14qrgt0  42852  pell1qrge1  42863  pell1qrgap  42867  pellfundge  42875  pellfundex  42879  pellfund14  42891  rmspecsqrtnq  42899  rmxypos  42940  ltrmynn0  42941  ltrmxnn0  42942  jm2.24nn  42952  jm2.17b  42954  jm2.17c  42955  jm2.24  42956  congadd  42959  congsym  42961  congneg  42962  congid  42964  mzpcong  42965  acongrep  42973  acongeq  42976  jm2.18  42981  jm2.19  42986  jm2.23  42989  jm2.25  42992  jm2.26lem3  42994  jm2.15nn0  42996  jm2.16nn0  42997  jm2.27a  42998  jm2.27c  43000  jm3.1lem1  43010  idomsubgmo  43186  sqrtcval  43634  inductionexd  44148  imo72b2lem0  44158  imo72b2  44165  dvgrat  44305  radcnvrat  44307  binomcxplemnn0  44342  binomcxplemnotnn0  44349  cncmpmax  45030  rnmptlb  45241  zltlesub  45287  infxrpnf  45445  xrpnf  45484  fmul01  45581  fmul01lt1lem1  45585  climdivf  45613  sumnnodd  45631  climinf2lem  45707  limsup10exlem  45773  climliminf  45807  dfxlim2v  45848  xlimliminflimsup  45863  dvdivbd  45924  volge0  45962  stoweidlem1  46002  stoweidlem16  46017  stoweidlem18  46019  stoweidlem24  46025  stoweidlem26  46027  stoweidlem36  46037  stoweidlem38  46039  stoweidlem41  46042  stoweidlem42  46043  stoweidlem44  46045  stoweidlem45  46046  stoweidlem48  46049  stoweidlem62  46063  wallispilem5  46070  stirlinglem1  46075  stirlinglem5  46079  stirlinglem7  46081  stirlinglem8  46082  stirlinglem9  46083  stirlinglem11  46085  fourierdlem4  46112  fourierdlem10  46118  fourierdlem37  46145  fourierdlem47  46154  fourierdlem72  46179  fourierdlem74  46181  fourierdlem79  46186  fourierdlem82  46189  fourierdlem89  46196  fourierdlem91  46198  fourierdlem93  46200  fourierdlem103  46210  fourierdlem104  46211  fourierdlem112  46219  etransclem24  46259  etransclem25  46260  etransclem28  46263  etransclem37  46272  etransclem38  46273  etransclem44  46279  meaiuninc3v  46485  vonicclem1  46684  pimconstlt0  46702  smfsuplem1  46812  rlimdmafv  47181  rlimdmafv2  47262  2elfz2melfz  47322  iccpartgtprec  47424  iccpartlt  47428  iccpartgtl  47430  sqrtpwpw2p  47542  fmtnodvds  47548  goldbachthlem1  47549  lighneallem4a  47612  perfectALTVlem1  47725  uhgrimgrlim  47991  cznnring  48266  altgsumbcALT  48357  expnegico01  48523  flnn0div2ge  48538  rege1logbrege0  48563  fllogbd  48565  nnpw2blen  48585  nnolog2flm1  48595  dignn0ldlem  48607  dignn0flhalflem1  48620  dignn0flhalflem2  48621  eenglngeehlnmlem2  48743  itsclc0yqsol  48769  2itscp  48786  itscnhlinecirc02plem1  48787  itscnhlinecirc02plem2  48788  inlinecirc02p  48792