Theorem breqtrrd 5117

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  marypha1lem  9317  marypha2  9323  infsupprpr  9390  unxpwdom  9475  ttrcltr  9606  onadju  10085  nnadju  10089  cfss  10156  tskuni  10674  ltexnq  10866  lt2addmuld  12371  div4p1lem1div2  12376  nn0le2x  12435  mul2lt0rgt0  12995  prodge0ld  13000  ge2halflem1  13007  xrmax1  13074  xrmax2  13075  max1ALT  13085  qbtwnxr  13099  xleadd1a  13152  xlt2add  13159  xlesubadd  13162  xmulgt0  13182  xlemul1a  13187  xov1plusxeqvd  13398  uzsubsubfz  13446  fzctr  13540  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  ccatdmss  14489  ccatws1n0  14540  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  chnub  18528  eqgen  19093  lagsubg  19107  pgpfi  19517  sylow2alem2  19530  sylow2a  19531  sylow3lem4  19542  efgsrel  19646  odadd1  19760  odadd2  19761  gexex  19765  lt6abl  19807  dprd2d2  19958  dmdprdpr  19963  ablfacrp2  19981  ablfac1c  19985  pgpfaclem1  19995  ablfac2  20003  fincygsubgodd  20026  omndmul2  20045  dvdsrmul1  20287  unitmulclb  20299  subrguss  20502  rhmsubcrngc  20583  abvres  20746  znfld  21497  znunit  21500  ofldchr  21513  frlmisfrlm  21785  ply1coefsupp  22212  evl1gsumadd  22273  matgsum  22352  pm2mpcl  22712  psmetxrge0  24228  isxmet2d  24242  mettri  24267  xmettri3  24268  mettri3  24269  xmetrtri2  24271  prdsxmetlem  24283  imasdsf1olem  24288  xblss2ps  24316  blss2ps  24318  blss2  24319  blssps  24339  blss  24340  prdsbl  24406  dscmet  24487  nmge0  24532  nmmtri  24537  tngngp3  24571  nlmvscnlem2  24600  nrginvrcnlem  24606  nmoix  24644  nmoleub  24646  blcvx  24713  xrsxmet  24725  opnreen  24747  xrge0tsms  24750  icopnfcnv  24867  xrhmeo  24871  lebnumii  24892  pcophtb  24956  pi1grplem  24976  nmoleub2lem  25041  ipcau2  25161  tcphcphlem1  25162  ipcau  25165  ipcnlem2  25171  rrxcph  25319  minveclem2  25353  minveclem3b  25355  pjthlem1  25364  pjthlem2  25365  ivthlem3  25381  ivth2  25383  ovolfsf  25399  ovolsslem  25412  ovollb2lem  25416  ovollb2  25417  ovolctb  25418  ovolfiniun  25429  ovolicc1  25444  ovolicc2lem4  25448  ovolicc2  25450  nulmbl2  25464  unmbl  25465  ioombl1lem4  25489  uniioombllem4  25514  uniioombllem6  25516  volivth  25535  vitalilem4  25539  itg1ge0  25614  itg1ge0a  25639  itg1lea  25640  itg1climres  25642  mbfi1fseqlem5  25647  itg2ub  25661  itg2seq  25670  itg2uba  25671  itg2splitlem  25676  itg2split  25677  itg2monolem3  25680  itg2mono  25681  itg2i1fseq2  25684  itg2addlem  25686  iblss  25733  itggt0  25772  dvferm2lem  25917  dvlip  25925  dvivthlem1  25940  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  ftc1lem4  25973  ply1divmo  26068  ply1remlem  26097  fta1glem2  26101  idomrootle  26105  ig1pdvds  26112  plyeq0lem  26142  plydiveu  26233  fta1lem  26242  vieta1lem2  26246  aaliou3lem2  26278  aaliou3lem8  26280  ulmcn  26335  mtest  26340  itgulm  26344  radcnvlem1  26349  radcnvlt1  26354  dvradcnv  26357  pserdvlem2  26365  abelthlem2  26369  abelthlem6  26373  abelthlem7  26375  abelthlem9  26377  tangtx  26441  sinq12gt0  26443  sineq0  26460  cosordlem  26466  tanord  26474  tanregt0  26475  logrnaddcl  26510  logcj  26542  argregt0  26546  argrege0  26547  argimgt0  26548  argimlt0  26549  logimul  26550  logneg2  26551  logdivlti  26556  divlogrlim  26571  logcnlem3  26580  logcnlem4  26581  dvlog2lem  26588  logtayl  26596  rpcxpcl  26612  cxpsqrtlem  26638  cxpaddle  26689  isosctrlem1  26755  asinlem3a  26807  asinlem3  26808  asinneg  26823  asinsinlem  26828  asinsin  26829  atanlogaddlem  26850  atanlogadd  26851  atanlogsublem  26852  atanlogsub  26853  atantan  26860  atanbndlem  26862  atantayl  26874  leibpi  26879  birthdaylem3  26890  areaf  26898  cxploglim  26915  jensenlem2  26925  jensen  26926  logdiflbnd  26932  harmonicbnd4  26948  fsumharmonic  26949  zetacvg  26952  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamcvg2  26992  wilthlem2  27006  wilthimp  27009  ftalem1  27010  ftalem2  27011  ftalem5  27014  basellem6  27023  basellem8  27025  basellem9  27026  chtge0  27049  chtublem  27149  logexprlim  27163  perfectlem1  27167  bcmax  27216  bposlem1  27222  bposlem2  27223  bposlem6  27227  bposlem7  27228  lgsdilem2  27271  lgsqrlem4  27287  lgsquadlem1  27318  2lgsoddprmlem2  27347  2sqlem3  27358  2sqlem8  27364  2sqblem  27369  2sqmod  27374  chebbnd1lem2  27408  chtppilimlem1  27411  chtppilim  27413  chto1ub  27414  vmadivsum  27420  rplogsumlem1  27422  rplogsumlem2  27423  dchrisum0lem1a  27424  rpvmasumlem  27425  dchrisumlem1  27427  dchrisumlem2  27428  dchrvmasumlem2  27436  dchrisum0flblem1  27446  dchrisum0flblem2  27447  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem3  27457  dchrisum0  27458  mudivsum  27468  mulogsumlem  27469  mulog2sumlem1  27472  mulog2sumlem2  27473  2vmadivsumlem  27478  chpdifbndlem1  27491  selberg3lem1  27495  selberg4lem1  27498  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntibndlem3  27530  pntlemd  27532  pntlemc  27533  pntlemb  27535  pntlemg  27536  pntlemh  27537  pntlemr  27540  pntlemf  27543  pntlemo  27545  abvcxp  27553  ostth2lem1  27556  padicabv  27568  ostth2lem2  27572  ostth2lem3  27573  ostth2lem4  27574  ostth2  27575  ostth3  27576  nodense  27631  nogt01o  27635  nosupbnd2lem1  27654  noetasuplem3  27674  maxs1  27704  maxs2  27705  eqscut3  27765  cofcutr  27868  cofcutrtime  27871  addsuniflem  27944  negsunif  27997  ssltmul2  28087  precsexlem11  28155  abssge0  28183  sleabs  28186  onscutlt  28201  om2noseqlt  28229  zsoring  28332  expsgt0  28360  halfcut  28378  addhalfcut  28379  tgcgr4  28509  legso  28577  krippenlem  28668  midex  28715  oppperpex  28731  ttgcontlem1  28863  axpaschlem  28918  axcontlem8  28949  upgrex  29070  nbfusgrlevtxm1  29355  finsumvtxdgeven  29531  wwlksnextproplem3  29889  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  32742  eliccelico  32760  elicoelioo  32761  bcm1n  32777  fsumiunle  32812  sgnmul  32818  nexple  32827  expevenpos  32829  pfxlsw2ccat  32931  wrdt2ind  32934  xrge0tsmsd  33042  gsumwrd2dccatlem  33046  psgnfzto1stlem  33069  cycpmco2lem4  33098  cycpmco2lem5  33099  cyc3conja  33126  archirngz  33158  archiabllem2c  33164  rprmasso2  33491  rprmirred  33496  1arithufdlem3  33511  lbslelsp  33610  fedgmullem2  33643  extdggt0  33670  evls1fldgencl  33683  fldextrspunlem1  33688  extdgfialglem1  33705  algextdeglem8  33737  rtelextdg2lem  33739  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  madjusmdetlem2  33841  locfinreflem  33853  xrge0iifiso  33948  gsumesum  34072  esumcst  34076  esumpcvgval  34091  esumcvg  34099  esumiun  34107  measssd  34228  measunl  34229  omssubadd  34313  carsgclctunlem3  34333  pmeasmono  34337  sibfof  34353  oddpwdc  34367  eulerpartlemgc  34375  iwrdsplit  34400  ballotlemsgt1  34524  ballotlemsel1i  34526  signsply0  34564  signstfvc  34587  signsvtp  34596  signsvfpn  34598  fdvposlt  34612  fdvneggt  34613  fdvnegge  34615  logdivsqrle  34663  hgt750lemf  34666  tgoldbachgtde  34673  swrdwlk  35171  subfaclim  35232  erdszelem7  35241  erdszelem8  35242  cvmliftlem2  35330  snmlff  35373  sinccvglem  35716  climlec3  35778  faclim  35790  fnejoin1  36412  poimirlem12  37671  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem23  37682  poimirlem28  37687  broucube  37693  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  itg2addnclem  37710  itg2addnclem3  37712  itg2gt0cn  37714  itggt0cn  37729  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anclem8  37739  isbnd3  37823  ssbnd  37827  heiborlem8  37857  bfplem2  37862  rrncmslem  37871  rrnequiv  37874  rrntotbnd  37875  lcv1  39139  lsatcv0eq  39145  lsatcvat3  39150  cvlsupr2  39441  hlatlej2  39474  cvrval4N  39512  cvratlem  39519  atcvr0eq  39524  2atlt  39537  atbtwnex  39546  athgt  39554  1cvrat  39574  ps-1  39575  hlatexch3N  39578  hlatexch4  39579  3atlem2  39582  atcvrlln2  39617  lplnexllnN  39662  4atlem3a  39695  4atlem10b  39703  4atlem11b  39706  4atlem12b  39709  2lplnja  39717  dalemply  39752  dalemsly  39753  dalem1  39757  dalem6  39766  dalem7  39767  dalem-cly  39769  dalem11  39772  dalem12  39773  dalem16  39777  dalem17  39778  dalem38  39808  dalem44  39814  dalem61  39831  lnatexN  39877  lncvrat  39880  lncmp  39881  paddasslem2  39919  dalawlem3  39971  dalawlem6  39974  dalawlem11  39979  lhpmcvr  40121  lhp2atne  40132  lhp2at0ne  40134  lautj  40191  trlval4  40286  cdlemc2  40290  cdlemc5  40293  cdleme3b  40327  cdleme11c  40359  cdleme19a  40401  cdleme20j  40416  cdleme22f  40444  cdleme23c  40449  cdleme26f2ALTN  40462  cdleme26f2  40463  cdleme35fnpq  40547  cdleme48bw  40600  cdlemg10a  40738  cdlemg11b  40740  cdlemg17g  40765  cdlemg18c  40778  cdlemi1  40916  cdlemk52  41052  dia2dimlem1  41162  dihord1  41316  dihjatcclem4  41519  lcmineqlem15  42135  lcmineqlem19  42139  lcmineqlem22  42142  aks4d1lem1  42154  aks4d1p1p4  42163  aks4d1p1p5  42167  aks4d1p2  42169  aks4d1p3  42170  aks4d1p6  42173  aks4d1p7d1  42174  aks4d1p7  42175  aks4d1p8  42179  aks4d1p9  42180  aks6d1c1p6  42206  aks6d1c1  42208  aks6d1c2  42222  sticksstones7  42244  aks6d1c7lem1  42272  unitscyglem4  42290  dvdsexpnn0  42426  prjspner01  42717  flt4lem5  42742  fltnltalem  42754  fltnlta  42755  3cubeslem1  42776  eldioph2lem1  42852  lzenom  42862  irrapxlem1  42914  irrapxlem4  42917  irrapxlem5  42918  pell14qrgt0  42951  pell1qrge1  42962  pell1qrgap  42966  pellfundge  42974  pellfundex  42978  pellfund14  42990  rmspecsqrtnq  42998  rmxypos  43039  ltrmynn0  43040  ltrmxnn0  43041  jm2.24nn  43051  jm2.17b  43053  jm2.17c  43054  jm2.24  43055  congadd  43058  congsym  43060  congneg  43061  congid  43063  mzpcong  43064  acongrep  43072  acongeq  43075  jm2.18  43080  jm2.19  43085  jm2.23  43088  jm2.25  43091  jm2.26lem3  43093  jm2.15nn0  43095  jm2.16nn0  43096  jm2.27a  43097  jm2.27c  43099  jm3.1lem1  43109  idomsubgmo  43285  sqrtcval  43733  inductionexd  44247  imo72b2lem0  44257  imo72b2  44264  dvgrat  44404  radcnvrat  44406  binomcxplemnn0  44441  binomcxplemnotnn0  44448  cncmpmax  45128  rnmptlb  45339  zltlesub  45385  infxrpnf  45543  xrpnf  45582  fmul01  45679  fmul01lt1lem1  45683  climdivf  45711  sumnnodd  45729  climinf2lem  45803  limsup10exlem  45869  climliminf  45903  dfxlim2v  45944  xlimliminflimsup  45959  dvdivbd  46020  volge0  46058  stoweidlem1  46098  stoweidlem16  46113  stoweidlem18  46115  stoweidlem24  46121  stoweidlem26  46123  stoweidlem36  46133  stoweidlem38  46135  stoweidlem41  46138  stoweidlem42  46139  stoweidlem44  46141  stoweidlem45  46142  stoweidlem48  46145  stoweidlem62  46159  wallispilem5  46166  stirlinglem1  46171  stirlinglem5  46175  stirlinglem7  46177  stirlinglem8  46178  stirlinglem9  46179  stirlinglem11  46181  fourierdlem4  46208  fourierdlem10  46214  fourierdlem37  46241  fourierdlem47  46250  fourierdlem72  46275  fourierdlem74  46277  fourierdlem79  46282  fourierdlem82  46285  fourierdlem89  46292  fourierdlem91  46294  fourierdlem93  46296  fourierdlem103  46306  fourierdlem104  46307  fourierdlem112  46315  etransclem24  46355  etransclem25  46356  etransclem28  46359  etransclem37  46368  etransclem38  46369  etransclem44  46375  meaiuninc3v  46581  vonicclem1  46780  pimconstlt0  46798  smfsuplem1  46908  chnerlem1  46979  rlimdmafv  47276  rlimdmafv2  47357  2elfz2melfz  47417  iccpartgtprec  47519  iccpartlt  47523  iccpartgtl  47525  sqrtpwpw2p  47637  fmtnodvds  47643  goldbachthlem1  47644  lighneallem4a  47707  perfectALTVlem1  47820  uhgrimgrlim  48086  cznnring  48361  altgsumbcALT  48452  expnegico01  48618  flnn0div2ge  48633  rege1logbrege0  48658  fllogbd  48660  nnpw2blen  48680  nnolog2flm1  48690  dignn0ldlem  48702  dignn0flhalflem1  48715  dignn0flhalflem2  48716  eenglngeehlnmlem2  48838  itsclc0yqsol  48864  2itscp  48881  itscnhlinecirc02plem1  48882  itscnhlinecirc02plem2  48883  inlinecirc02p  48887