Theorem breqtrrd 5125

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  marypha1lem  9338  marypha2  9344  infsupprpr  9411  unxpwdom  9496  ttrcltr  9627  onadju  10106  nnadju  10110  cfss  10177  tskuni  10696  ltexnq  10888  lt2addmuld  12393  div4p1lem1div2  12398  nn0le2x  12457  mul2lt0rgt0  13012  prodge0ld  13017  ge2halflem1  13024  xrmax1  13092  xrmax2  13093  max1ALT  13103  qbtwnxr  13117  xleadd1a  13170  xlt2add  13177  xlesubadd  13180  xmulgt0  13200  xlemul1a  13205  xov1plusxeqvd  13416  uzsubsubfz  13464  fzctr  13558  subfzo0  13710  flflp1  13729  fldiv4lem1div2uz2  13758  ceilge  13767  modge0  13801  modlt  13802  modid  13818  m1modge3gt1  13843  modaddmodup  13859  sermono  13959  seqf1olem1  13966  seqf1olem2  13967  sqgt0  14051  sqge0  14061  leexp1a  14100  nnlesq  14130  expnbnd  14157  expmulnbnd  14160  discr1  14164  facwordi  14214  faclbnd5  14223  nfile  14284  hashdom  14304  hashgt23el  14349  fi1uzind  14432  brfi1indALT  14435  ccatdmss  14507  ccatws1n0  14558  swrds2  14865  cjmulge0  15071  resqrtcl  15178  absge0  15212  sqreulem  15285  amgm2  15295  rlimdm  15476  rlimge0  15506  reccn2  15522  climle  15565  climserle  15588  isercoll2  15594  iseraltlem1  15607  iseralt  15610  isumclim2  15683  isumclim3  15684  isumge0  15691  fsumless  15721  cvgcmp  15741  cvgcmpce  15743  abscvgcvg  15744  isumsup2  15771  isumltss  15773  climcndslem1  15774  climcnds  15776  supcvg  15781  harmonic  15784  expcnv  15789  explecnv  15790  cvgrat  15808  mertenslem1  15809  mertenslem2  15810  clim2div  15814  ntrivcvgtail  15825  iprodclim2  15924  iprodclim3  15925  efcvg  16010  ege2le3  16015  efaddlem  16018  eftlub  16036  effsumlt  16038  tanhlt1  16087  ef01bndlem  16111  sin02gt0  16119  rpnnen2lem4  16144  ruclem2  16159  ruclem3  16160  ruclem9  16165  iddvdsexp  16208  dvdsadd  16231  dvdsfac  16255  dvdsexp2im  16256  dvdsmod  16258  3dvds  16260  omoe  16293  sumeven  16316  divalglem1  16323  flodddiv4t2lthalf  16347  bitsfzo  16364  bitsmod  16365  bitscmp  16367  bitsinv1lem  16370  sadcaddlem  16386  sadadd3  16390  sadaddlem  16395  dvdssqim  16483  dvdsexpim  16484  dvdsmulgcd  16485  nn0seqcvgd  16499  dvdslcm  16527  lcmgcdlem  16535  dvdslcmf  16560  lcmfunsnlem2lem2  16568  mulgcddvds  16584  qredeq  16586  cncongr2  16597  sqnprm  16631  isprm6  16643  dvdszzq  16650  prmdvdsbc  16655  nonsq  16688  hashdvds  16704  prmdiv  16714  odzdvds  16725  pythagtriplem4  16749  pcpre1  16772  pcdvdsb  16799  pcz  16811  pcprmpw2  16812  pcaddlem  16818  pcadd  16819  pcadd2  16820  pcmpt  16822  pcmptdvds  16824  fldivp1  16827  pcfaclem  16828  pockthlem  16835  prmreclem1  16846  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  4sqlem6  16873  4sqlem8  16875  4sqlem11  16885  4sqlem12  16886  4sqlem14  16888  4sqlem16  16890  vdwlem3  16913  vdwlem9  16919  vdwlem10  16920  vdwlem12  16922  ramub1lem2  16957  prmgap  16989  prmgaplcm  16990  prmgapprmo  16992  mreexexd  17573  invfuc  17903  ple1  18353  chnub  18547  eqgen  19112  lagsubg  19126  pgpfi  19536  sylow2alem2  19549  sylow2a  19550  sylow3lem4  19561  efgsrel  19665  odadd1  19779  odadd2  19780  gexex  19784  lt6abl  19826  dprd2d2  19977  dmdprdpr  19982  ablfacrp2  20000  ablfac1c  20004  pgpfaclem1  20014  ablfac2  20022  fincygsubgodd  20045  omndmul2  20064  dvdsrmul1  20307  unitmulclb  20319  subrguss  20522  rhmsubcrngc  20603  abvres  20766  znfld  21517  znunit  21520  ofldchr  21533  frlmisfrlm  21805  ply1coefsupp  22243  evl1gsumadd  22304  matgsum  22383  pm2mpcl  22743  psmetxrge0  24259  isxmet2d  24273  mettri  24298  xmettri3  24299  mettri3  24300  xmetrtri2  24302  prdsxmetlem  24314  imasdsf1olem  24319  xblss2ps  24347  blss2ps  24349  blss2  24350  blssps  24370  blss  24371  prdsbl  24437  dscmet  24518  nmge0  24563  nmmtri  24568  tngngp3  24602  nlmvscnlem2  24631  nrginvrcnlem  24637  nmoix  24675  nmoleub  24677  blcvx  24744  xrsxmet  24756  opnreen  24778  xrge0tsms  24781  icopnfcnv  24898  xrhmeo  24902  lebnumii  24923  pcophtb  24987  pi1grplem  25007  nmoleub2lem  25072  ipcau2  25192  tcphcphlem1  25193  ipcau  25196  ipcnlem2  25202  rrxcph  25350  minveclem2  25384  minveclem3b  25386  pjthlem1  25395  pjthlem2  25396  ivthlem3  25412  ivth2  25414  ovolfsf  25430  ovolsslem  25443  ovollb2lem  25447  ovollb2  25448  ovolctb  25449  ovolfiniun  25460  ovolicc1  25475  ovolicc2lem4  25479  ovolicc2  25481  nulmbl2  25495  unmbl  25496  ioombl1lem4  25520  uniioombllem4  25545  uniioombllem6  25547  volivth  25566  vitalilem4  25570  itg1ge0  25645  itg1ge0a  25670  itg1lea  25671  itg1climres  25673  mbfi1fseqlem5  25678  itg2ub  25692  itg2seq  25701  itg2uba  25702  itg2splitlem  25707  itg2split  25708  itg2monolem3  25711  itg2mono  25712  itg2i1fseq2  25715  itg2addlem  25717  iblss  25764  itggt0  25803  dvferm2lem  25948  dvlip  25956  dvivthlem1  25971  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem3  25993  ftc1lem4  26004  ply1divmo  26099  ply1remlem  26128  fta1glem2  26132  idomrootle  26136  ig1pdvds  26143  plyeq0lem  26173  plydiveu  26264  fta1lem  26273  vieta1lem2  26277  aaliou3lem2  26309  aaliou3lem8  26311  ulmcn  26366  mtest  26371  itgulm  26375  radcnvlem1  26380  radcnvlt1  26385  dvradcnv  26388  pserdvlem2  26396  abelthlem2  26400  abelthlem6  26404  abelthlem7  26406  abelthlem9  26408  tangtx  26472  sinq12gt0  26474  sineq0  26491  cosordlem  26497  tanord  26505  tanregt0  26506  logrnaddcl  26541  logcj  26573  argregt0  26577  argrege0  26578  argimgt0  26579  argimlt0  26580  logimul  26581  logneg2  26582  logdivlti  26587  divlogrlim  26602  logcnlem3  26611  logcnlem4  26612  dvlog2lem  26619  logtayl  26627  rpcxpcl  26643  cxpsqrtlem  26669  cxpaddle  26720  isosctrlem1  26786  asinlem3a  26838  asinlem3  26839  asinneg  26854  asinsinlem  26859  asinsin  26860  atanlogaddlem  26881  atanlogadd  26882  atanlogsublem  26883  atanlogsub  26884  atantan  26891  atanbndlem  26893  atantayl  26905  leibpi  26910  birthdaylem3  26921  areaf  26929  cxploglim  26946  jensenlem2  26956  jensen  26957  logdiflbnd  26963  harmonicbnd4  26979  fsumharmonic  26980  zetacvg  26983  lgamgulmlem2  26998  lgamgulmlem3  26999  lgamcvg2  27023  wilthlem2  27037  wilthimp  27040  ftalem1  27041  ftalem2  27042  ftalem5  27045  basellem6  27054  basellem8  27056  basellem9  27057  chtge0  27080  chtublem  27180  logexprlim  27194  perfectlem1  27198  bcmax  27247  bposlem1  27253  bposlem2  27254  bposlem6  27258  bposlem7  27259  lgsdilem2  27302  lgsqrlem4  27318  lgsquadlem1  27349  2lgsoddprmlem2  27378  2sqlem3  27389  2sqlem8  27395  2sqblem  27400  2sqmod  27405  chebbnd1lem2  27439  chtppilimlem1  27442  chtppilim  27444  chto1ub  27445  vmadivsum  27451  rplogsumlem1  27453  rplogsumlem2  27454  dchrisum0lem1a  27455  rpvmasumlem  27456  dchrisumlem1  27458  dchrisumlem2  27459  dchrvmasumlem2  27467  dchrisum0flblem1  27477  dchrisum0flblem2  27478  dchrisum0lem1b  27484  dchrisum0lem1  27485  dchrisum0lem2a  27486  dchrisum0lem3  27488  dchrisum0  27489  mudivsum  27499  mulogsumlem  27500  mulog2sumlem1  27503  mulog2sumlem2  27504  2vmadivsumlem  27509  chpdifbndlem1  27522  selberg3lem1  27526  selberg4lem1  27529  pntrlog2bndlem1  27546  pntrlog2bndlem2  27547  pntrlog2bndlem3  27548  pntrlog2bndlem4  27549  pntpbnd1a  27554  pntpbnd1  27555  pntpbnd2  27556  pntibndlem2  27560  pntibndlem3  27561  pntlemd  27563  pntlemc  27564  pntlemb  27566  pntlemg  27567  pntlemh  27568  pntlemr  27571  pntlemf  27574  pntlemo  27576  abvcxp  27584  ostth2lem1  27587  padicabv  27599  ostth2lem2  27603  ostth2lem3  27604  ostth2lem4  27605  ostth2  27606  ostth3  27607  nodense  27662  nogt01o  27666  nosupbnd2lem1  27685  noetasuplem3  27705  maxs1  27739  maxs2  27740  eqscut3  27800  cofcutr  27904  cofcutrtime  27907  addsuniflem  27981  negsunif  28035  ssltmul2  28128  precsexlem11  28196  abssge0  28224  sleabs  28227  onscutlt  28243  om2noseqlt  28278  zsoring  28386  expsgt0  28414  halfcut  28435  addhalfcut  28436  bdayfinbndlem1  28444  elreno2  28472  tgcgr4  28584  legso  28652  krippenlem  28743  midex  28790  oppperpex  28806  ttgcontlem1  28938  axpaschlem  28994  axcontlem8  29025  upgrex  29146  nbfusgrlevtxm1  29431  finsumvtxdgeven  29607  wwlksnextproplem3  29965  clwlkclwwlk2  30059  clwlkclwwlkfolem  30063  clwwlkndivn  30136  ex-ind-dvds  30517  nvabs  30728  nmooge0  30823  nmoolb  30827  siii  30909  minvecolem2  30931  minvecolem4  30936  minvecolem5  30937  hlipgt0  30970  normge0  31182  normpyc  31202  pjhthlem1  31447  pjige0i  31746  nmoplb  31963  nmfnlb  31980  branmfn  32161  pjssdif2i  32230  stlei  32296  xlt2addrd  32818  eliccelico  32836  elicoelioo  32837  bcm1n  32854  fsumiunle  32889  sgnmul  32895  nexple  32904  expevenpos  32906  pfxlsw2ccat  33011  wrdt2ind  33014  xrge0tsmsd  33134  gsumwrd2dccatlem  33138  psgnfzto1stlem  33161  cycpmco2lem4  33190  cycpmco2lem5  33191  cyc3conja  33218  archirngz  33250  archiabllem2c  33256  rprmasso2  33586  rprmirred  33591  1arithufdlem3  33606  vietadeg1  33713  lbslelsp  33733  fedgmullem2  33766  extdggt0  33793  evls1fldgencl  33806  fldextrspunlem1  33811  extdgfialglem1  33828  algextdeglem8  33860  rtelextdg2lem  33862  cos9thpiminplylem1  33918  cos9thpiminplylem2  33919  madjusmdetlem2  33964  locfinreflem  33976  xrge0iifiso  34071  gsumesum  34195  esumcst  34199  esumpcvgval  34214  esumcvg  34222  esumiun  34230  measssd  34351  measunl  34352  omssubadd  34436  carsgclctunlem3  34456  pmeasmono  34460  sibfof  34476  oddpwdc  34490  eulerpartlemgc  34498  iwrdsplit  34523  ballotlemsgt1  34647  ballotlemsel1i  34649  signsply0  34687  signstfvc  34710  signsvtp  34719  signsvfpn  34721  fdvposlt  34735  fdvneggt  34736  fdvnegge  34738  logdivsqrle  34786  hgt750lemf  34789  tgoldbachgtde  34796  swrdwlk  35300  subfaclim  35361  erdszelem7  35370  erdszelem8  35371  cvmliftlem2  35459  snmlff  35502  sinccvglem  35845  climlec3  35907  faclim  35919  fnejoin1  36541  poimirlem12  37802  poimirlem17  37807  poimirlem19  37809  poimirlem20  37810  poimirlem23  37813  poimirlem28  37818  broucube  37824  mblfinlem2  37828  mblfinlem3  37829  mblfinlem4  37830  ismblfin  37831  itg2addnclem  37841  itg2addnclem3  37843  itg2gt0cn  37845  itggt0cn  37860  ftc1anclem5  37867  ftc1anclem7  37869  ftc1anclem8  37870  isbnd3  37954  ssbnd  37958  heiborlem8  37988  bfplem2  37993  rrncmslem  38002  rrnequiv  38005  rrntotbnd  38006  lcv1  39336  lsatcv0eq  39342  lsatcvat3  39347  cvlsupr2  39638  hlatlej2  39671  cvrval4N  39709  cvratlem  39716  atcvr0eq  39721  2atlt  39734  atbtwnex  39743  athgt  39751  1cvrat  39771  ps-1  39772  hlatexch3N  39775  hlatexch4  39776  3atlem2  39779  atcvrlln2  39814  lplnexllnN  39859  4atlem3a  39892  4atlem10b  39900  4atlem11b  39903  4atlem12b  39906  2lplnja  39914  dalemply  39949  dalemsly  39950  dalem1  39954  dalem6  39963  dalem7  39964  dalem-cly  39966  dalem11  39969  dalem12  39970  dalem16  39974  dalem17  39975  dalem38  40005  dalem44  40011  dalem61  40028  lnatexN  40074  lncvrat  40077  lncmp  40078  paddasslem2  40116  dalawlem3  40168  dalawlem6  40171  dalawlem11  40176  lhpmcvr  40318  lhp2atne  40329  lhp2at0ne  40331  lautj  40388  trlval4  40483  cdlemc2  40487  cdlemc5  40490  cdleme3b  40524  cdleme11c  40556  cdleme19a  40598  cdleme20j  40613  cdleme22f  40641  cdleme23c  40646  cdleme26f2ALTN  40659  cdleme26f2  40660  cdleme35fnpq  40744  cdleme48bw  40797  cdlemg10a  40935  cdlemg11b  40937  cdlemg17g  40962  cdlemg18c  40975  cdlemi1  41113  cdlemk52  41249  dia2dimlem1  41359  dihord1  41513  dihjatcclem4  41716  lcmineqlem15  42332  lcmineqlem19  42336  lcmineqlem22  42339  aks4d1lem1  42351  aks4d1p1p4  42360  aks4d1p1p5  42364  aks4d1p2  42366  aks4d1p3  42367  aks4d1p6  42370  aks4d1p7d1  42371  aks4d1p7  42372  aks4d1p8  42376  aks4d1p9  42377  aks6d1c1p6  42403  aks6d1c1  42405  aks6d1c2  42419  sticksstones7  42441  aks6d1c7lem1  42469  unitscyglem4  42487  dvdsexpnn0  42626  prjspner01  42905  flt4lem5  42930  fltnltalem  42942  fltnlta  42943  3cubeslem1  42963  eldioph2lem1  43039  lzenom  43049  irrapxlem1  43101  irrapxlem4  43104  irrapxlem5  43105  pell14qrgt0  43138  pell1qrge1  43149  pell1qrgap  43153  pellfundge  43161  pellfundex  43165  pellfund14  43177  rmspecsqrtnq  43185  rmxypos  43226  ltrmynn0  43227  ltrmxnn0  43228  jm2.24nn  43238  jm2.17b  43240  jm2.17c  43241  jm2.24  43242  congadd  43245  congsym  43247  congneg  43248  congid  43250  mzpcong  43251  acongrep  43259  acongeq  43262  jm2.18  43267  jm2.19  43272  jm2.23  43275  jm2.25  43278  jm2.26lem3  43280  jm2.15nn0  43282  jm2.16nn0  43283  jm2.27a  43284  jm2.27c  43286  jm3.1lem1  43296  idomsubgmo  43472  sqrtcval  43919  inductionexd  44433  imo72b2lem0  44443  imo72b2  44450  dvgrat  44590  radcnvrat  44592  binomcxplemnn0  44627  binomcxplemnotnn0  44634  cncmpmax  45314  rnmptlb  45524  zltlesub  45570  infxrpnf  45727  xrpnf  45766  fmul01  45863  fmul01lt1lem1  45867  climdivf  45895  sumnnodd  45913  climinf2lem  45987  limsup10exlem  46053  climliminf  46087  dfxlim2v  46128  xlimliminflimsup  46143  dvdivbd  46204  volge0  46242  stoweidlem1  46282  stoweidlem16  46297  stoweidlem18  46299  stoweidlem24  46305  stoweidlem26  46307  stoweidlem36  46317  stoweidlem38  46319  stoweidlem41  46322  stoweidlem42  46323  stoweidlem44  46325  stoweidlem45  46326  stoweidlem48  46329  stoweidlem62  46343  wallispilem5  46350  stirlinglem1  46355  stirlinglem5  46359  stirlinglem7  46361  stirlinglem8  46362  stirlinglem9  46363  stirlinglem11  46365  fourierdlem4  46392  fourierdlem10  46398  fourierdlem37  46425  fourierdlem47  46434  fourierdlem72  46459  fourierdlem74  46461  fourierdlem79  46466  fourierdlem82  46469  fourierdlem89  46476  fourierdlem91  46478  fourierdlem93  46480  fourierdlem103  46490  fourierdlem104  46491  fourierdlem112  46499  etransclem24  46539  etransclem25  46540  etransclem28  46543  etransclem37  46552  etransclem38  46553  etransclem44  46559  meaiuninc3v  46765  vonicclem1  46964  pimconstlt0  46982  smfsuplem1  47092  chnerlem1  47163  rlimdmafv  47460  rlimdmafv2  47541  2elfz2melfz  47601  iccpartgtprec  47703  iccpartlt  47707  iccpartgtl  47709  sqrtpwpw2p  47821  fmtnodvds  47827  goldbachthlem1  47828  lighneallem4a  47891  perfectALTVlem1  48004  uhgrimgrlim  48270  cznnring  48545  altgsumbcALT  48636  expnegico01  48801  flnn0div2ge  48816  rege1logbrege0  48841  fllogbd  48843  nnpw2blen  48863  nnolog2flm1  48873  dignn0ldlem  48885  dignn0flhalflem1  48898  dignn0flhalflem2  48899  eenglngeehlnmlem2  49021  itsclc0yqsol  49047  2itscp  49064  itscnhlinecirc02plem1  49065  itscnhlinecirc02plem2  49066  inlinecirc02p  49070