Theorem breqtrrd 5138

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  marypha1lem  9391  marypha2  9397  infsupprpr  9464  unxpwdom  9549  ttrcltr  9683  onadju  10184  nnadju  10188  cfss  10255  tskuni  10774  ltexnq  10966  lt2addmuld  12500  div4p1lem1div2  12505  nn0le2x  12564  mul2lt0rgt0  13127  prodge0ld  13132  ge2halflem1  13139  xrmax1  13207  xrmax2  13208  max1ALT  13218  qbtwnxr  13232  xleadd1a  13285  xlt2add  13292  xlesubadd  13295  xmulgt0  13315  xlemul1a  13320  xov1plusxeqvd  13531  uzsubsubfz  13581  fzctr  13675  subfzo0  13828  flflp1  13847  fldiv4lem1div2uz2  13876  ceilge  13885  modge0  13919  modlt  13920  modid  13936  m1modge3gt1  13961  modaddmodup  13977  sermono  14077  seqf1olem1  14084  seqf1olem2  14085  sqgt0  14169  sqge0  14179  leexp1a  14218  nnlesq  14248  expnbnd  14275  expmulnbnd  14278  discr1  14282  facwordi  14332  faclbnd5  14341  nfile  14402  hashdom  14422  hashgt23el  14468  fi1uzind  14551  brfi1indALT  14554  ccatdmss  14626  ccatws1n0  14677  swrds2  14984  sgnmul  15151  cjmulge0  15204  resqrtcl  15311  absge0  15345  sqreulem  15418  amgm2  15428  rlimdm  15609  rlimge0  15639  reccn2  15655  climle  15698  climserle  15721  isercoll2  15727  iseraltlem1  15740  iseralt  15743  isumclim2  15816  isumclim3  15817  isumge0  15824  fsumless  15855  cvgcmp  15875  cvgcmpce  15877  abscvgcvg  15878  isumsup2  15907  isumltss  15909  climcndslem1  15910  climcnds  15912  supcvg  15917  harmonic  15920  expcnv  15925  explecnv  15926  cvgrat  15944  mertenslem1  15945  mertenslem2  15946  clim2div  15950  ntrivcvgtail  15961  iprodclim2  16060  iprodclim3  16061  efcvg  16145  ege2le3  16150  efaddlem  16153  eftlub  16171  effsumlt  16173  tanhlt1  16222  ef01bndlem  16246  sin02gt0  16254  rpnnen2lem4  16279  ruclem2  16294  ruclem3  16295  ruclem9  16300  iddvdsexp  16343  dvdsadd  16366  dvdsfac  16390  dvdsexp2im  16391  dvdsmod  16393  3dvds  16395  omoe  16428  sumeven  16451  divalglem1  16458  flodddiv4t2lthalf  16482  bitsfzo  16499  bitsmod  16500  bitscmp  16502  bitsinv1lem  16505  sadcaddlem  16521  sadadd3  16525  sadaddlem  16530  dvdssqim  16618  dvdsexpim  16619  dvdsmulgcd  16620  nn0seqcvgd  16634  dvdslcm  16662  lcmgcdlem  16670  dvdslcmf  16695  lcmfunsnlem2lem2  16703  mulgcddvds  16719  qredeq  16721  cncongr2  16732  sqnprm  16767  isprm6  16779  dvdszzq  16786  prmdvdsbc  16791  nonsq  16824  hashdvds  16840  prmdiv  16850  odzdvds  16861  pythagtriplem4  16885  pcpre1  16908  pcdvdsb  16935  pcz  16947  pcprmpw2  16948  pcaddlem  16954  pcadd  16955  pcadd2  16956  pcmpt  16958  pcmptdvds  16960  fldivp1  16963  pcfaclem  16964  pockthlem  16971  prmreclem1  16982  prmreclem3  16984  prmreclem5  16986  prmreclem6  16987  4sqlem6  17009  4sqlem8  17011  4sqlem11  17021  4sqlem12  17022  4sqlem14  17024  4sqlem16  17026  vdwlem3  17049  vdwlem9  17055  vdwlem10  17056  vdwlem12  17058  ramub1lem2  17093  prmgap  17125  prmgaplcm  17126  prmgapprmo  17128  mreexexd  17710  invfuc  18040  ple1  18490  chnub  18684  eqgen  19255  lagsubg  19272  pgpfi  19681  sylow2alem2  19694  sylow2a  19695  sylow3lem4  19706  efgsrel  19810  odadd1  19924  odadd2  19925  gexex  19929  lt6abl  19971  dprd2d2  20122  dmdprdpr  20127  ablfacrp2  20145  ablfac1c  20149  pgpfaclem1  20159  ablfac2  20167  fincygsubgodd  20190  omndmul2  20209  dvdsrmul1  20458  unitmulclb  20470  subrguss  20697  rhmsubcrngc  20778  abvres  20945  znfld  21721  znunit  21724  ofldchr  21737  frlmisfrlm  22009  ply1coefsupp  22468  evl1gsumadd  22529  matgsum  22605  pm2mpcl  22965  psmetxrge0  24481  isxmet2d  24495  mettri  24520  xmettri3  24521  mettri3  24522  xmetrtri2  24524  prdsxmetlem  24536  imasdsf1olem  24541  xblss2ps  24569  blss2ps  24571  blss2  24572  blssps  24592  blss  24593  prdsbl  24659  dscmet  24740  nmge0  24785  nmmtri  24790  tngngp3  24824  nlmvscnlem2  24853  nrginvrcnlem  24859  nmoix  24897  nmoleub  24899  blcvx  24966  xrsxmet  24978  opnreen  25000  xrge0tsms  25003  icopnfcnv  25112  xrhmeo  25116  lebnumii  25136  pcophtb  25199  pi1grplem  25219  nmoleub2lem  25284  ipcau2  25404  tcphcphlem1  25405  ipcau  25408  ipcnlem2  25414  rrxcph  25562  minveclem2  25596  minveclem3b  25598  pjthlem1  25607  pjthlem2  25608  ivthlem3  25623  ivth2  25625  ovolfsf  25641  ovolsslem  25654  ovollb2lem  25658  ovollb2  25659  ovolctb  25660  ovolfiniun  25671  ovolicc1  25686  ovolicc2lem4  25690  ovolicc2  25692  nulmbl2  25706  unmbl  25707  ioombl1lem4  25731  uniioombllem4  25756  uniioombllem6  25758  volivth  25777  vitalilem4  25781  itg1ge0  25856  itg1ge0a  25881  itg1lea  25882  itg1climres  25884  mbfi1fseqlem5  25889  itg2ub  25903  itg2seq  25912  itg2uba  25913  itg2splitlem  25918  itg2split  25919  itg2monolem3  25922  itg2mono  25923  itg2i1fseq2  25926  itg2addlem  25928  iblss  25975  itggt0  26014  dvferm2lem  26156  dvlip  26163  dvivthlem1  26178  dvfsumlem2  26197  dvfsumlem3  26198  ftc1lem4  26209  ply1divmo  26304  ply1remlem  26333  fta1glem2  26337  idomrootle  26341  ig1pdvds  26348  plyeq0lem  26378  plydiveu  26470  fta1lem  26479  vieta1lem2  26483  aaliou3lem2  26517  aaliou3lem8  26519  ulmcn  26573  mtest  26578  itgulm  26582  radcnvlem1  26587  radcnvlt1  26592  dvradcnv  26595  pserdvlem2  26602  abelthlem2  26606  abelthlem6  26610  abelthlem7  26612  abelthlem9  26614  tangtx  26681  sinq12gt0  26683  sineq0  26700  cosordlem  26706  tanord  26714  tanregt0  26715  logrnaddcl  26750  logcj  26782  argregt0  26786  argrege0  26787  argimgt0  26788  argimlt0  26789  logimul  26790  logneg2  26791  logdivlti  26796  divlogrlim  26811  logcnlem3  26820  logcnlem4  26821  dvlog2lem  26828  logtayl  26836  rpcxpcl  26852  cxpsqrtlem  26878  cxpaddle  26928  isosctrlem1  26994  asinlem3a  27046  asinlem3  27047  asinneg  27062  asinsinlem  27067  asinsin  27068  atanlogaddlem  27089  atanlogadd  27090  atanlogsublem  27091  atanlogsub  27092  atantan  27099  atanbndlem  27101  atantayl  27113  leibpi  27118  birthdaylem3  27129  areaf  27137  cxploglim  27153  jensenlem2  27163  jensen  27164  logdiflbnd  27170  harmonicbnd4  27186  fsumharmonic  27187  zetacvg  27190  lgamgulmlem2  27205  lgamgulmlem3  27206  lgamcvg2  27230  wilthlem2  27244  wilthimp  27247  ftalem1  27248  ftalem2  27249  ftalem5  27252  basellem6  27261  basellem8  27263  basellem9  27264  chtge0  27287  chtublem  27386  logexprlim  27400  perfectlem1  27404  bcmax  27453  bposlem1  27459  bposlem2  27460  bposlem6  27464  bposlem7  27465  lgsdilem2  27508  lgsqrlem4  27524  lgsquadlem1  27555  2lgsoddprmlem2  27584  2sqlem3  27595  2sqlem8  27601  2sqblem  27606  2sqmod  27611  chebbnd1lem2  27645  chtppilimlem1  27648  chtppilim  27650  chto1ub  27651  vmadivsum  27657  rplogsumlem1  27659  rplogsumlem2  27660  dchrisum0lem1a  27661  rpvmasumlem  27662  dchrisumlem1  27664  dchrisumlem2  27665  dchrvmasumlem2  27673  dchrisum0flblem1  27683  dchrisum0flblem2  27684  dchrisum0lem1b  27690  dchrisum0lem1  27691  dchrisum0lem2a  27692  dchrisum0lem3  27694  dchrisum0  27695  mudivsum  27705  mulogsumlem  27706  mulog2sumlem1  27709  mulog2sumlem2  27710  2vmadivsumlem  27715  chpdifbndlem1  27728  selberg3lem1  27732  selberg4lem1  27735  pntrlog2bndlem1  27752  pntrlog2bndlem2  27753  pntrlog2bndlem3  27754  pntrlog2bndlem4  27755  pntpbnd1a  27760  pntpbnd1  27761  pntpbnd2  27762  pntibndlem2  27766  pntibndlem3  27767  pntlemd  27769  pntlemc  27770  pntlemb  27772  pntlemg  27773  pntlemh  27774  pntlemr  27777  pntlemf  27780  pntlemo  27782  abvcxp  27790  ostth2lem1  27793  padicabv  27805  ostth2lem2  27809  ostth2lem3  27810  ostth2lem4  27811  ostth2  27812  ostth3  27813  nodense  27867  nogt01o  27871  nosupbnd2lem1  27890  noetasuplem3  27910  maxs1  27944  maxs2  27945  eqcuts3  28008  cofcutr  28128  cofcutrtime  28131  addsuniflem  28205  negsunif  28259  sltmuls2  28352  precsexlem11  28421  abssge0  28449  leabss  28452  oncutlt  28468  om2noseqlt  28503  zsoring  28613  expsgt0  28641  halfcut  28662  addhalfcut  28663  bdayfinbndlem1  28671  elreno2  28699  tgcgr4  28811  legso  28879  krippenlem  28978  midex  29029  oppperpex  29045  prlngmid2  29222  prlngsymquadopp  29226  quadcgrprlng  29227  ttgcontlem1  29245  axpaschlem  29301  axcontlem8  29332  upgrex  29453  nbfusgrlevtxm1  29738  finsumvtxdgeven  29913  wwlksnextproplem3  30271  clwlkclwwlk2  30365  clwlkclwwlkfolem  30369  clwwlkndivn  30442  ex-ind-dvds  30823  nvabs  31035  nmooge0  31130  nmoolb  31134  siii  31216  minvecolem2  31238  minvecolem4  31243  minvecolem5  31244  hlipgt0  31277  normge0  31489  normpyc  31509  pjhthlem1  31754  pjige0i  32053  nmoplb  32270  nmfnlb  32287  branmfn  32468  pjssdif2i  32537  stlei  32603  xlt2addrd  33115  eliccelico  33133  elicoelioo  33134  bcm1n  33151  fsumiunle  33184  nexple  33188  expevenpos  33190  pfxlsw2ccat  33279  wrdt2ind  33282  xrge0tsmsd  33402  gsumwrd2dccatlem  33406  psgnfzto1stlem  33429  cycpmco2lem4  33458  cycpmco2lem5  33459  cyc3conja  33486  archirngz  33518  archiabllem2c  33524  rprmasso2  33825  rprmirred  33830  1arithufdlem3  33845  vietadeg1  33977  lbslelsp  33997  fedgmullem2  34029  extdggt0  34056  evls1fldgencl  34069  fldextrspunlem1  34074  extdgfialglem1  34091  algextdeglem8  34123  rtelextdg2lem  34125  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  madjusmdetlem2  34227  locfinreflem  34239  xrge0iifiso  34334  gsumesum  34458  esumcst  34462  esumpcvgval  34477  esumcvg  34485  esumiun  34493  measssd  34614  measunl  34615  omssubadd  34699  carsgclctunlem3  34719  pmeasmono  34723  sibfof  34739  oddpwdc  34753  eulerpartlemgc  34761  iwrdsplit  34786  ballotlemsgt1  34910  ballotlemsel1i  34912  signsply0  34947  signstfvc  34970  signsvtp  34979  signsvfpn  34981  fdvposlt  34995  fdvneggt  34996  fdvnegge  34998  logdivsqrle  35046  hgt750lemf  35049  tgoldbachgtde  35056  swrdwlk  35627  subfaclim  35688  erdszelem7  35697  erdszelem8  35698  cvmliftlem2  35786  snmlff  35829  sinccvglem  36172  climlec3  36234  faclim  36246  fnejoin1  36907  poimirlem12  38311  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem23  38322  poimirlem28  38327  broucube  38333  mblfinlem2  38337  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  itg2addnclem  38350  itg2addnclem3  38352  itg2gt0cn  38354  itggt0cn  38369  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  isbnd3  38463  ssbnd  38467  heiborlem8  38497  bfplem2  38502  rrncmslem  38511  rrnequiv  38514  rrntotbnd  38515  lcv1  39843  lsatcv0eq  39849  lsatcvat3  39854  cvlsupr2  40145  hlatlej2  40178  cvrval4N  40216  cvratlem  40223  atcvr0eq  40228  2atlt  40241  atbtwnex  40250  athgt  40258  1cvrat  40278  ps-1  40279  hlatexch3N  40282  hlatexch4  40283  3atlem2  40286  atcvrlln2  40321  lplnexllnN  40366  4atlem3a  40399  4atlem10b  40407  4atlem11b  40410  4atlem12b  40413  2lplnja  40421  dalemply  40456  dalemsly  40457  dalem1  40461  dalem6  40470  dalem7  40471  dalem-cly  40473  dalem11  40476  dalem12  40477  dalem16  40481  dalem17  40482  dalem38  40512  dalem44  40518  dalem61  40535  lnatexN  40581  lncvrat  40584  lncmp  40585  paddasslem2  40623  dalawlem3  40675  dalawlem6  40678  dalawlem11  40683  lhpmcvr  40825  lhp2atne  40836  lhp2at0ne  40838  lautj  40895  trlval4  40990  cdlemc2  40994  cdlemc5  40997  cdleme3b  41031  cdleme11c  41063  cdleme19a  41105  cdleme20j  41120  cdleme22f  41148  cdleme23c  41153  cdleme26f2ALTN  41166  cdleme26f2  41167  cdleme35fnpq  41251  cdleme48bw  41304  cdlemg10a  41442  cdlemg11b  41444  cdlemg17g  41469  cdlemg18c  41482  cdlemi1  41620  cdlemk52  41756  dia2dimlem1  41866  dihord1  42020  dihjatcclem4  42223  lcmineqlem15  42838  lcmineqlem19  42842  lcmineqlem22  42845  aks4d1lem1  42857  aks4d1p1p4  42866  aks4d1p1p5  42870  aks4d1p2  42872  aks4d1p3  42873  aks4d1p6  42876  aks4d1p7d1  42877  aks4d1p7  42878  aks4d1p8  42882  aks4d1p9  42883  aks6d1c1p6  42909  aks6d1c1  42911  aks6d1c2  42925  sticksstones7  42947  aks6d1c7lem1  42975  unitscyglem4  42993  dvdsexpnn0  43123  prjspner01  43385  flt4lem5  43410  fltnltalem  43422  fltnlta  43423  3cubeslem1  43443  eldioph2lem1  43519  lzenom  43529  irrapxlem1  43577  irrapxlem4  43580  irrapxlem5  43581  pell14qrgt0  43614  pell1qrge1  43625  pell1qrgap  43629  pellfundge  43637  pellfundex  43641  pellfund14  43653  rmspecsqrtnq  43661  rmxypos  43702  ltrmynn0  43703  ltrmxnn0  43704  jm2.24nn  43714  jm2.17b  43716  jm2.17c  43717  jm2.24  43718  congadd  43721  congsym  43723  congneg  43724  congid  43726  mzpcong  43727  acongrep  43735  acongeq  43738  jm2.18  43743  jm2.19  43748  jm2.23  43751  jm2.25  43754  jm2.26lem3  43756  jm2.15nn0  43758  jm2.16nn0  43759  jm2.27a  43760  jm2.27c  43762  jm3.1lem1  43772  idomsubgmo  43948  sqrtcval  44395  inductionexd  44909  imo72b2lem0  44919  imo72b2  44926  dvgrat  45050  radcnvrat  45052  binomcxplemnn0  45087  binomcxplemnotnn0  45094  cncmpmax  45780  rnmptlb  45986  zltlesub  46032  infxrpnf  46188  xrpnf  46227  fmul01  46324  fmul01lt1lem1  46328  climdivf  46356  sumnnodd  46374  climinf2lem  46448  limsup10exlem  46514  climliminf  46548  dfxlim2v  46589  xlimliminflimsup  46604  dvdivbd  46665  volge0  46703  stoweidlem1  46743  stoweidlem16  46758  stoweidlem18  46760  stoweidlem24  46766  stoweidlem26  46768  stoweidlem36  46778  stoweidlem38  46780  stoweidlem41  46783  stoweidlem42  46784  stoweidlem44  46786  stoweidlem45  46787  stoweidlem48  46790  stoweidlem62  46804  wallispilem5  46811  stirlinglem1  46816  stirlinglem5  46820  stirlinglem7  46822  stirlinglem8  46823  stirlinglem9  46824  stirlinglem11  46826  fourierdlem4  46853  fourierdlem10  46859  fourierdlem37  46886  fourierdlem47  46895  fourierdlem72  46920  fourierdlem74  46922  fourierdlem79  46927  fourierdlem82  46930  fourierdlem89  46937  fourierdlem91  46939  fourierdlem93  46941  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  etransclem24  47000  etransclem25  47001  etransclem28  47004  etransclem37  47013  etransclem38  47014  etransclem44  47020  meaiuninc3v  47226  vonicclem1  47425  pimconstlt0  47443  smfsuplem1  47553  chnerlem1  47626  rlimdmafv  47942  rlimdmafv2  48023  2elfz2melfz  48083  2timesltsq  48143  muldvdsfacgt  48151  iccpartgtprec  48197  iccpartlt  48201  iccpartgtl  48203  sqrtpwpw2p  48318  fmtnodvds  48324  goldbachthlem1  48325  lighneallem4a  48388  nprmdvdsfacm1lem1  48400  perfectALTVlem1  48514  uhgrimgrlim  48780  cznnring  49055  altgsumbcALT  49161  expnegico01  49326  flnn0div2ge  49341  rege1logbrege0  49366  fllogbd  49368  nnpw2blen  49388  nnolog2flm1  49398  dignn0ldlem  49410  dignn0flhalflem1  49423  dignn0flhalflem2  49424  eenglngeehlnmlem2  49546  itsclc0yqsol  49572  2itscp  49589  itscnhlinecirc02plem1  49590  itscnhlinecirc02plem2  49591  inlinecirc02p  49595