Theorem breqtrrd 5123

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  marypha1lem  9327  marypha2  9333  infsupprpr  9400  unxpwdom  9485  ttrcltr  9616  onadju  10095  nnadju  10099  cfss  10166  tskuni  10684  ltexnq  10876  lt2addmuld  12381  div4p1lem1div2  12386  nn0le2x  12445  mul2lt0rgt0  13005  prodge0ld  13010  ge2halflem1  13017  xrmax1  13084  xrmax2  13085  max1ALT  13095  qbtwnxr  13109  xleadd1a  13162  xlt2add  13169  xlesubadd  13172  xmulgt0  13192  xlemul1a  13197  xov1plusxeqvd  13408  uzsubsubfz  13456  fzctr  13550  subfzo0  13702  flflp1  13721  fldiv4lem1div2uz2  13750  ceilge  13759  modge0  13793  modlt  13794  modid  13810  m1modge3gt1  13835  modaddmodup  13851  sermono  13951  seqf1olem1  13958  seqf1olem2  13959  sqgt0  14043  sqge0  14053  leexp1a  14092  nnlesq  14122  expnbnd  14149  expmulnbnd  14152  discr1  14156  facwordi  14206  faclbnd5  14215  nfile  14276  hashdom  14296  hashgt23el  14341  fi1uzind  14424  brfi1indALT  14427  ccatdmss  14499  ccatws1n0  14550  swrds2  14857  cjmulge0  15063  resqrtcl  15170  absge0  15204  sqreulem  15277  amgm2  15287  rlimdm  15468  rlimge0  15498  reccn2  15514  climle  15557  climserle  15580  isercoll2  15586  iseraltlem1  15599  iseralt  15602  isumclim2  15675  isumclim3  15676  isumge0  15683  fsumless  15713  cvgcmp  15733  cvgcmpce  15735  abscvgcvg  15736  isumsup2  15763  isumltss  15765  climcndslem1  15766  climcnds  15768  supcvg  15773  harmonic  15776  expcnv  15781  explecnv  15782  cvgrat  15800  mertenslem1  15801  mertenslem2  15802  clim2div  15806  ntrivcvgtail  15817  iprodclim2  15916  iprodclim3  15917  efcvg  16002  ege2le3  16007  efaddlem  16010  eftlub  16028  effsumlt  16030  tanhlt1  16079  ef01bndlem  16103  sin02gt0  16111  rpnnen2lem4  16136  ruclem2  16151  ruclem3  16152  ruclem9  16157  iddvdsexp  16200  dvdsadd  16223  dvdsfac  16247  dvdsexp2im  16248  dvdsmod  16250  3dvds  16252  omoe  16285  sumeven  16308  divalglem1  16315  flodddiv4t2lthalf  16339  bitsfzo  16356  bitsmod  16357  bitscmp  16359  bitsinv1lem  16362  sadcaddlem  16378  sadadd3  16382  sadaddlem  16387  dvdssqim  16475  dvdsexpim  16476  dvdsmulgcd  16477  nn0seqcvgd  16491  dvdslcm  16519  lcmgcdlem  16527  dvdslcmf  16552  lcmfunsnlem2lem2  16560  mulgcddvds  16576  qredeq  16578  cncongr2  16589  sqnprm  16623  isprm6  16635  dvdszzq  16642  prmdvdsbc  16647  nonsq  16680  hashdvds  16696  prmdiv  16706  odzdvds  16717  pythagtriplem4  16741  pcpre1  16764  pcdvdsb  16791  pcz  16803  pcprmpw2  16804  pcaddlem  16810  pcadd  16811  pcadd2  16812  pcmpt  16814  pcmptdvds  16816  fldivp1  16819  pcfaclem  16820  pockthlem  16827  prmreclem1  16838  prmreclem3  16840  prmreclem5  16842  prmreclem6  16843  4sqlem6  16865  4sqlem8  16867  4sqlem11  16877  4sqlem12  16878  4sqlem14  16880  4sqlem16  16882  vdwlem3  16905  vdwlem9  16911  vdwlem10  16912  vdwlem12  16914  ramub1lem2  16949  prmgap  16981  prmgaplcm  16982  prmgapprmo  16984  mreexexd  17564  invfuc  17894  ple1  18344  chnub  18538  eqgen  19103  lagsubg  19117  pgpfi  19527  sylow2alem2  19540  sylow2a  19541  sylow3lem4  19552  efgsrel  19656  odadd1  19770  odadd2  19771  gexex  19775  lt6abl  19817  dprd2d2  19968  dmdprdpr  19973  ablfacrp2  19991  ablfac1c  19995  pgpfaclem1  20005  ablfac2  20013  fincygsubgodd  20036  omndmul2  20055  dvdsrmul1  20297  unitmulclb  20309  subrguss  20512  rhmsubcrngc  20593  abvres  20756  znfld  21507  znunit  21510  ofldchr  21523  frlmisfrlm  21795  ply1coefsupp  22222  evl1gsumadd  22283  matgsum  22362  pm2mpcl  22722  psmetxrge0  24238  isxmet2d  24252  mettri  24277  xmettri3  24278  mettri3  24279  xmetrtri2  24281  prdsxmetlem  24293  imasdsf1olem  24298  xblss2ps  24326  blss2ps  24328  blss2  24329  blssps  24349  blss  24350  prdsbl  24416  dscmet  24497  nmge0  24542  nmmtri  24547  tngngp3  24581  nlmvscnlem2  24610  nrginvrcnlem  24616  nmoix  24654  nmoleub  24656  blcvx  24723  xrsxmet  24735  opnreen  24757  xrge0tsms  24760  icopnfcnv  24877  xrhmeo  24881  lebnumii  24902  pcophtb  24966  pi1grplem  24986  nmoleub2lem  25051  ipcau2  25171  tcphcphlem1  25172  ipcau  25175  ipcnlem2  25181  rrxcph  25329  minveclem2  25363  minveclem3b  25365  pjthlem1  25374  pjthlem2  25375  ivthlem3  25391  ivth2  25393  ovolfsf  25409  ovolsslem  25422  ovollb2lem  25426  ovollb2  25427  ovolctb  25428  ovolfiniun  25439  ovolicc1  25454  ovolicc2lem4  25458  ovolicc2  25460  nulmbl2  25474  unmbl  25475  ioombl1lem4  25499  uniioombllem4  25524  uniioombllem6  25526  volivth  25545  vitalilem4  25549  itg1ge0  25624  itg1ge0a  25649  itg1lea  25650  itg1climres  25652  mbfi1fseqlem5  25657  itg2ub  25671  itg2seq  25680  itg2uba  25681  itg2splitlem  25686  itg2split  25687  itg2monolem3  25690  itg2mono  25691  itg2i1fseq2  25694  itg2addlem  25696  iblss  25743  itggt0  25782  dvferm2lem  25927  dvlip  25935  dvivthlem1  25950  dvfsumlem2  25970  dvfsumlem2OLD  25971  dvfsumlem3  25972  ftc1lem4  25983  ply1divmo  26078  ply1remlem  26107  fta1glem2  26111  idomrootle  26115  ig1pdvds  26122  plyeq0lem  26152  plydiveu  26243  fta1lem  26252  vieta1lem2  26256  aaliou3lem2  26288  aaliou3lem8  26290  ulmcn  26345  mtest  26350  itgulm  26354  radcnvlem1  26359  radcnvlt1  26364  dvradcnv  26367  pserdvlem2  26375  abelthlem2  26379  abelthlem6  26383  abelthlem7  26385  abelthlem9  26387  tangtx  26451  sinq12gt0  26453  sineq0  26470  cosordlem  26476  tanord  26484  tanregt0  26485  logrnaddcl  26520  logcj  26552  argregt0  26556  argrege0  26557  argimgt0  26558  argimlt0  26559  logimul  26560  logneg2  26561  logdivlti  26566  divlogrlim  26581  logcnlem3  26590  logcnlem4  26591  dvlog2lem  26598  logtayl  26606  rpcxpcl  26622  cxpsqrtlem  26648  cxpaddle  26699  isosctrlem1  26765  asinlem3a  26817  asinlem3  26818  asinneg  26833  asinsinlem  26838  asinsin  26839  atanlogaddlem  26860  atanlogadd  26861  atanlogsublem  26862  atanlogsub  26863  atantan  26870  atanbndlem  26872  atantayl  26884  leibpi  26889  birthdaylem3  26900  areaf  26908  cxploglim  26925  jensenlem2  26935  jensen  26936  logdiflbnd  26942  harmonicbnd4  26958  fsumharmonic  26959  zetacvg  26962  lgamgulmlem2  26977  lgamgulmlem3  26978  lgamcvg2  27002  wilthlem2  27016  wilthimp  27019  ftalem1  27020  ftalem2  27021  ftalem5  27024  basellem6  27033  basellem8  27035  basellem9  27036  chtge0  27059  chtublem  27159  logexprlim  27173  perfectlem1  27177  bcmax  27226  bposlem1  27232  bposlem2  27233  bposlem6  27237  bposlem7  27238  lgsdilem2  27281  lgsqrlem4  27297  lgsquadlem1  27328  2lgsoddprmlem2  27357  2sqlem3  27368  2sqlem8  27374  2sqblem  27379  2sqmod  27384  chebbnd1lem2  27418  chtppilimlem1  27421  chtppilim  27423  chto1ub  27424  vmadivsum  27430  rplogsumlem1  27432  rplogsumlem2  27433  dchrisum0lem1a  27434  rpvmasumlem  27435  dchrisumlem1  27437  dchrisumlem2  27438  dchrvmasumlem2  27446  dchrisum0flblem1  27456  dchrisum0flblem2  27457  dchrisum0lem1b  27463  dchrisum0lem1  27464  dchrisum0lem2a  27465  dchrisum0lem3  27467  dchrisum0  27468  mudivsum  27478  mulogsumlem  27479  mulog2sumlem1  27482  mulog2sumlem2  27483  2vmadivsumlem  27488  chpdifbndlem1  27501  selberg3lem1  27505  selberg4lem1  27508  pntrlog2bndlem1  27525  pntrlog2bndlem2  27526  pntrlog2bndlem3  27527  pntrlog2bndlem4  27528  pntpbnd1a  27533  pntpbnd1  27534  pntpbnd2  27535  pntibndlem2  27539  pntibndlem3  27540  pntlemd  27542  pntlemc  27543  pntlemb  27545  pntlemg  27546  pntlemh  27547  pntlemr  27550  pntlemf  27553  pntlemo  27555  abvcxp  27563  ostth2lem1  27566  padicabv  27578  ostth2lem2  27582  ostth2lem3  27583  ostth2lem4  27584  ostth2  27585  ostth3  27586  nodense  27641  nogt01o  27645  nosupbnd2lem1  27664  noetasuplem3  27684  maxs1  27714  maxs2  27715  eqscut3  27775  cofcutr  27878  cofcutrtime  27881  addsuniflem  27954  negsunif  28007  ssltmul2  28097  precsexlem11  28165  abssge0  28193  sleabs  28196  onscutlt  28211  om2noseqlt  28239  zsoring  28342  expsgt0  28370  halfcut  28388  addhalfcut  28389  tgcgr4  28519  legso  28587  krippenlem  28678  midex  28725  oppperpex  28741  ttgcontlem1  28873  axpaschlem  28929  axcontlem8  28960  upgrex  29081  nbfusgrlevtxm1  29366  finsumvtxdgeven  29542  wwlksnextproplem3  29900  clwlkclwwlk2  29994  clwlkclwwlkfolem  29998  clwwlkndivn  30071  ex-ind-dvds  30452  nvabs  30663  nmooge0  30758  nmoolb  30762  siii  30844  minvecolem2  30866  minvecolem4  30871  minvecolem5  30872  hlipgt0  30905  normge0  31117  normpyc  31137  pjhthlem1  31382  pjige0i  31681  nmoplb  31898  nmfnlb  31915  branmfn  32096  pjssdif2i  32165  stlei  32231  xlt2addrd  32753  eliccelico  32771  elicoelioo  32772  bcm1n  32788  fsumiunle  32823  sgnmul  32829  nexple  32838  expevenpos  32840  pfxlsw2ccat  32942  wrdt2ind  32945  xrge0tsmsd  33053  gsumwrd2dccatlem  33057  psgnfzto1stlem  33080  cycpmco2lem4  33109  cycpmco2lem5  33110  cyc3conja  33137  archirngz  33169  archiabllem2c  33175  rprmasso2  33502  rprmirred  33507  1arithufdlem3  33522  lbslelsp  33621  fedgmullem2  33654  extdggt0  33681  evls1fldgencl  33694  fldextrspunlem1  33699  extdgfialglem1  33716  algextdeglem8  33748  rtelextdg2lem  33750  cos9thpiminplylem1  33806  cos9thpiminplylem2  33807  madjusmdetlem2  33852  locfinreflem  33864  xrge0iifiso  33959  gsumesum  34083  esumcst  34087  esumpcvgval  34102  esumcvg  34110  esumiun  34118  measssd  34239  measunl  34240  omssubadd  34324  carsgclctunlem3  34344  pmeasmono  34348  sibfof  34364  oddpwdc  34378  eulerpartlemgc  34386  iwrdsplit  34411  ballotlemsgt1  34535  ballotlemsel1i  34537  signsply0  34575  signstfvc  34598  signsvtp  34607  signsvfpn  34609  fdvposlt  34623  fdvneggt  34624  fdvnegge  34626  logdivsqrle  34674  hgt750lemf  34677  tgoldbachgtde  34684  swrdwlk  35182  subfaclim  35243  erdszelem7  35252  erdszelem8  35253  cvmliftlem2  35341  snmlff  35384  sinccvglem  35727  climlec3  35789  faclim  35801  fnejoin1  36423  poimirlem12  37682  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  poimirlem28  37698  broucube  37704  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  itg2addnclem  37721  itg2addnclem3  37723  itg2gt0cn  37725  itggt0cn  37740  ftc1anclem5  37747  ftc1anclem7  37749  ftc1anclem8  37750  isbnd3  37834  ssbnd  37838  heiborlem8  37868  bfplem2  37873  rrncmslem  37882  rrnequiv  37885  rrntotbnd  37886  lcv1  39150  lsatcv0eq  39156  lsatcvat3  39161  cvlsupr2  39452  hlatlej2  39485  cvrval4N  39523  cvratlem  39530  atcvr0eq  39535  2atlt  39548  atbtwnex  39557  athgt  39565  1cvrat  39585  ps-1  39586  hlatexch3N  39589  hlatexch4  39590  3atlem2  39593  atcvrlln2  39628  lplnexllnN  39673  4atlem3a  39706  4atlem10b  39714  4atlem11b  39717  4atlem12b  39720  2lplnja  39728  dalemply  39763  dalemsly  39764  dalem1  39768  dalem6  39777  dalem7  39778  dalem-cly  39780  dalem11  39783  dalem12  39784  dalem16  39788  dalem17  39789  dalem38  39819  dalem44  39825  dalem61  39842  lnatexN  39888  lncvrat  39891  lncmp  39892  paddasslem2  39930  dalawlem3  39982  dalawlem6  39985  dalawlem11  39990  lhpmcvr  40132  lhp2atne  40143  lhp2at0ne  40145  lautj  40202  trlval4  40297  cdlemc2  40301  cdlemc5  40304  cdleme3b  40338  cdleme11c  40370  cdleme19a  40412  cdleme20j  40427  cdleme22f  40455  cdleme23c  40460  cdleme26f2ALTN  40473  cdleme26f2  40474  cdleme35fnpq  40558  cdleme48bw  40611  cdlemg10a  40749  cdlemg11b  40751  cdlemg17g  40776  cdlemg18c  40789  cdlemi1  40927  cdlemk52  41063  dia2dimlem1  41173  dihord1  41327  dihjatcclem4  41530  lcmineqlem15  42146  lcmineqlem19  42150  lcmineqlem22  42153  aks4d1lem1  42165  aks4d1p1p4  42174  aks4d1p1p5  42178  aks4d1p2  42180  aks4d1p3  42181  aks4d1p6  42184  aks4d1p7d1  42185  aks4d1p7  42186  aks4d1p8  42190  aks4d1p9  42191  aks6d1c1p6  42217  aks6d1c1  42219  aks6d1c2  42233  sticksstones7  42255  aks6d1c7lem1  42283  unitscyglem4  42301  dvdsexpnn0  42442  prjspner01  42733  flt4lem5  42758  fltnltalem  42770  fltnlta  42771  3cubeslem1  42791  eldioph2lem1  42867  lzenom  42877  irrapxlem1  42929  irrapxlem4  42932  irrapxlem5  42933  pell14qrgt0  42966  pell1qrge1  42977  pell1qrgap  42981  pellfundge  42989  pellfundex  42993  pellfund14  43005  rmspecsqrtnq  43013  rmxypos  43054  ltrmynn0  43055  ltrmxnn0  43056  jm2.24nn  43066  jm2.17b  43068  jm2.17c  43069  jm2.24  43070  congadd  43073  congsym  43075  congneg  43076  congid  43078  mzpcong  43079  acongrep  43087  acongeq  43090  jm2.18  43095  jm2.19  43100  jm2.23  43103  jm2.25  43106  jm2.26lem3  43108  jm2.15nn0  43110  jm2.16nn0  43111  jm2.27a  43112  jm2.27c  43114  jm3.1lem1  43124  idomsubgmo  43300  sqrtcval  43748  inductionexd  44262  imo72b2lem0  44272  imo72b2  44279  dvgrat  44419  radcnvrat  44421  binomcxplemnn0  44456  binomcxplemnotnn0  44463  cncmpmax  45143  rnmptlb  45354  zltlesub  45400  infxrpnf  45558  xrpnf  45597  fmul01  45694  fmul01lt1lem1  45698  climdivf  45726  sumnnodd  45744  climinf2lem  45818  limsup10exlem  45884  climliminf  45918  dfxlim2v  45959  xlimliminflimsup  45974  dvdivbd  46035  volge0  46073  stoweidlem1  46113  stoweidlem16  46128  stoweidlem18  46130  stoweidlem24  46136  stoweidlem26  46138  stoweidlem36  46148  stoweidlem38  46150  stoweidlem41  46153  stoweidlem42  46154  stoweidlem44  46156  stoweidlem45  46157  stoweidlem48  46160  stoweidlem62  46174  wallispilem5  46181  stirlinglem1  46186  stirlinglem5  46190  stirlinglem7  46192  stirlinglem8  46193  stirlinglem9  46194  stirlinglem11  46196  fourierdlem4  46223  fourierdlem10  46229  fourierdlem37  46256  fourierdlem47  46265  fourierdlem72  46290  fourierdlem74  46292  fourierdlem79  46297  fourierdlem82  46300  fourierdlem89  46307  fourierdlem91  46309  fourierdlem93  46311  fourierdlem103  46321  fourierdlem104  46322  fourierdlem112  46330  etransclem24  46370  etransclem25  46371  etransclem28  46374  etransclem37  46383  etransclem38  46384  etransclem44  46390  meaiuninc3v  46596  vonicclem1  46795  pimconstlt0  46813  smfsuplem1  46923  chnerlem1  46994  rlimdmafv  47291  rlimdmafv2  47372  2elfz2melfz  47432  iccpartgtprec  47534  iccpartlt  47538  iccpartgtl  47540  sqrtpwpw2p  47652  fmtnodvds  47658  goldbachthlem1  47659  lighneallem4a  47722  perfectALTVlem1  47835  uhgrimgrlim  48101  cznnring  48376  altgsumbcALT  48467  expnegico01  48633  flnn0div2ge  48648  rege1logbrege0  48673  fllogbd  48675  nnpw2blen  48695  nnolog2flm1  48705  dignn0ldlem  48717  dignn0flhalflem1  48730  dignn0flhalflem2  48731  eenglngeehlnmlem2  48853  itsclc0yqsol  48879  2itscp  48896  itscnhlinecirc02plem1  48897  itscnhlinecirc02plem2  48898  inlinecirc02p  48902