Theorem breqtrrd 5147

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  marypha1lem  9443  marypha2  9449  infsupprpr  9516  unxpwdom  9601  ttrcltr  9728  onadju  10206  nnadju  10210  cfss  10277  tskuni  10795  ltexnq  10987  lt2addmuld  12489  div4p1lem1div2  12494  nn0le2x  12553  mul2lt0rgt0  13110  prodge0ld  13115  ge2halflem1  13122  xrmax1  13189  xrmax2  13190  max1ALT  13200  qbtwnxr  13214  xleadd1a  13267  xlt2add  13274  xlesubadd  13277  xmulgt0  13297  xlemul1a  13302  xov1plusxeqvd  13513  uzsubsubfz  13561  fzctr  13655  subfzo0  13803  flflp1  13822  fldiv4lem1div2uz2  13851  ceilge  13860  modge0  13894  modlt  13895  modid  13911  m1modge3gt1  13934  modaddmodup  13950  sermono  14050  seqf1olem1  14057  seqf1olem2  14058  sqgt0  14142  sqge0  14152  leexp1a  14191  nnlesq  14221  expnbnd  14248  expmulnbnd  14251  discr1  14255  facwordi  14305  faclbnd5  14314  nfile  14375  hashdom  14395  hashgt23el  14440  fi1uzind  14523  brfi1indALT  14526  ccatws1n0  14648  swrds2  14957  cjmulge0  15163  resqrtcl  15270  absge0  15304  sqreulem  15376  amgm2  15386  rlimdm  15565  rlimge0  15595  reccn2  15611  climle  15654  climserle  15677  isercoll2  15683  iseraltlem1  15696  iseralt  15699  isumclim2  15772  isumclim3  15773  isumge0  15780  fsumless  15810  cvgcmp  15830  cvgcmpce  15832  abscvgcvg  15833  isumsup2  15860  isumltss  15862  climcndslem1  15863  climcnds  15865  supcvg  15870  harmonic  15873  expcnv  15878  explecnv  15879  cvgrat  15897  mertenslem1  15898  mertenslem2  15899  clim2div  15903  ntrivcvgtail  15914  iprodclim2  16013  iprodclim3  16014  efcvg  16099  ege2le3  16104  efaddlem  16107  eftlub  16125  effsumlt  16127  tanhlt1  16176  ef01bndlem  16200  sin02gt0  16208  rpnnen2lem4  16233  ruclem2  16248  ruclem3  16249  ruclem9  16254  iddvdsexp  16297  dvdsadd  16319  dvdsfac  16343  dvdsexp2im  16344  dvdsmod  16346  3dvds  16348  omoe  16381  sumeven  16404  divalglem1  16411  flodddiv4t2lthalf  16435  bitsfzo  16452  bitsmod  16453  bitscmp  16455  bitsinv1lem  16458  sadcaddlem  16474  sadadd3  16478  sadaddlem  16483  dvdssqim  16571  dvdsexpim  16572  dvdsmulgcd  16573  nn0seqcvgd  16587  dvdslcm  16615  lcmgcdlem  16623  dvdslcmf  16648  lcmfunsnlem2lem2  16656  mulgcddvds  16672  qredeq  16674  cncongr2  16685  sqnprm  16719  isprm6  16731  dvdszzq  16738  prmdvdsbc  16743  nonsq  16776  hashdvds  16792  prmdiv  16802  odzdvds  16813  pythagtriplem4  16837  pcpre1  16860  pcdvdsb  16887  pcz  16899  pcprmpw2  16900  pcaddlem  16906  pcadd  16907  pcadd2  16908  pcmpt  16910  pcmptdvds  16912  fldivp1  16915  pcfaclem  16916  pockthlem  16923  prmreclem1  16934  prmreclem3  16936  prmreclem5  16938  prmreclem6  16939  4sqlem6  16961  4sqlem8  16963  4sqlem11  16973  4sqlem12  16974  4sqlem14  16976  4sqlem16  16978  vdwlem3  17001  vdwlem9  17007  vdwlem10  17008  vdwlem12  17010  ramub1lem2  17045  prmgap  17077  prmgaplcm  17078  prmgapprmo  17080  mreexexd  17658  invfuc  17988  ple1  18438  eqgen  19162  lagsubg  19176  pgpfi  19584  sylow2alem2  19597  sylow2a  19598  sylow3lem4  19609  efgsrel  19713  odadd1  19827  odadd2  19828  gexex  19832  lt6abl  19874  dprd2d2  20025  dmdprdpr  20030  ablfacrp2  20048  ablfac1c  20052  pgpfaclem1  20062  ablfac2  20070  fincygsubgodd  20093  dvdsrmul1  20327  unitmulclb  20339  subrguss  20545  rhmsubcrngc  20626  abvres  20789  znfld  21519  znunit  21522  frlmisfrlm  21806  ply1coefsupp  22233  evl1gsumadd  22294  matgsum  22373  pm2mpcl  22733  psmetxrge0  24250  isxmet2d  24264  mettri  24289  xmettri3  24290  mettri3  24291  xmetrtri2  24293  prdsxmetlem  24305  imasdsf1olem  24310  xblss2ps  24338  blss2ps  24340  blss2  24341  blssps  24361  blss  24362  prdsbl  24428  dscmet  24509  nmge0  24554  nmmtri  24559  tngngp3  24593  nlmvscnlem2  24622  nrginvrcnlem  24628  nmoix  24666  nmoleub  24668  blcvx  24735  xrsxmet  24747  opnreen  24769  xrge0tsms  24772  icopnfcnv  24889  xrhmeo  24893  lebnumii  24914  pcophtb  24978  pi1grplem  24998  nmoleub2lem  25063  ipcau2  25184  tcphcphlem1  25185  ipcau  25188  ipcnlem2  25194  rrxcph  25342  minveclem2  25376  minveclem3b  25378  pjthlem1  25387  pjthlem2  25388  ivthlem3  25404  ivth2  25406  ovolfsf  25422  ovolsslem  25435  ovollb2lem  25439  ovollb2  25440  ovolctb  25441  ovolfiniun  25452  ovolicc1  25467  ovolicc2lem4  25471  ovolicc2  25473  nulmbl2  25487  unmbl  25488  ioombl1lem4  25512  uniioombllem4  25537  uniioombllem6  25539  volivth  25558  vitalilem4  25562  itg1ge0  25637  itg1ge0a  25662  itg1lea  25663  itg1climres  25665  mbfi1fseqlem5  25670  itg2ub  25684  itg2seq  25693  itg2uba  25694  itg2splitlem  25699  itg2split  25700  itg2monolem3  25703  itg2mono  25704  itg2i1fseq2  25707  itg2addlem  25709  iblss  25756  itggt0  25795  dvferm2lem  25940  dvlip  25948  dvivthlem1  25963  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  ftc1lem4  25996  ply1divmo  26091  ply1remlem  26120  fta1glem2  26124  idomrootle  26128  ig1pdvds  26135  plyeq0lem  26165  plydiveu  26256  fta1lem  26265  vieta1lem2  26269  aaliou3lem2  26301  aaliou3lem8  26303  ulmcn  26358  mtest  26363  itgulm  26367  radcnvlem1  26372  radcnvlt1  26377  dvradcnv  26380  pserdvlem2  26388  abelthlem2  26392  abelthlem6  26396  abelthlem7  26398  abelthlem9  26400  tangtx  26464  sinq12gt0  26466  sineq0  26483  cosordlem  26489  tanord  26497  tanregt0  26498  logrnaddcl  26533  logcj  26565  argregt0  26569  argrege0  26570  argimgt0  26571  argimlt0  26572  logimul  26573  logneg2  26574  logdivlti  26579  divlogrlim  26594  logcnlem3  26603  logcnlem4  26604  dvlog2lem  26611  logtayl  26619  rpcxpcl  26635  cxpsqrtlem  26661  cxpaddle  26712  isosctrlem1  26778  asinlem3a  26830  asinlem3  26831  asinneg  26846  asinsinlem  26851  asinsin  26852  atanlogaddlem  26873  atanlogadd  26874  atanlogsublem  26875  atanlogsub  26876  atantan  26883  atanbndlem  26885  atantayl  26897  leibpi  26902  birthdaylem3  26913  areaf  26921  cxploglim  26938  jensenlem2  26948  jensen  26949  logdiflbnd  26955  harmonicbnd4  26971  fsumharmonic  26972  zetacvg  26975  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamcvg2  27015  wilthlem2  27029  wilthimp  27032  ftalem1  27033  ftalem2  27034  ftalem5  27037  basellem6  27046  basellem8  27048  basellem9  27049  chtge0  27072  chtublem  27172  logexprlim  27186  perfectlem1  27190  bcmax  27239  bposlem1  27245  bposlem2  27246  bposlem6  27250  bposlem7  27251  lgsdilem2  27294  lgsqrlem4  27310  lgsquadlem1  27341  2lgsoddprmlem2  27370  2sqlem3  27381  2sqlem8  27387  2sqblem  27392  2sqmod  27397  chebbnd1lem2  27431  chtppilimlem1  27434  chtppilim  27436  chto1ub  27437  vmadivsum  27443  rplogsumlem1  27445  rplogsumlem2  27446  dchrisum0lem1a  27447  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrvmasumlem2  27459  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem3  27480  dchrisum0  27481  mudivsum  27491  mulogsumlem  27492  mulog2sumlem1  27495  mulog2sumlem2  27496  2vmadivsumlem  27501  chpdifbndlem1  27514  selberg3lem1  27518  selberg4lem1  27521  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem2  27552  pntibndlem3  27553  pntlemd  27555  pntlemc  27556  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemr  27563  pntlemf  27566  pntlemo  27568  abvcxp  27576  ostth2lem1  27579  padicabv  27591  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth2  27598  ostth3  27599  nodense  27654  nogt01o  27658  nosupbnd2lem1  27677  noetasuplem3  27697  maxs1  27727  maxs2  27728  cofcutr  27875  cofcutrtime  27878  addsuniflem  27951  negsunif  28004  ssltmul2  28091  precsexlem11  28158  abssge0  28186  sleabs  28189  om2noseqlt  28222  expsgt0  28332  halfcut  28333  addhalfcut  28336  tgcgr4  28456  legso  28524  krippenlem  28615  midex  28662  oppperpex  28678  ttgcontlem1  28810  axpaschlem  28865  axcontlem8  28896  upgrex  29017  nbfusgrlevtxm1  29302  finsumvtxdgeven  29478  wwlksnextproplem3  29839  clwlkclwwlk2  29930  clwlkclwwlkfolem  29934  clwwlkndivn  30007  ex-ind-dvds  30388  nvabs  30599  nmooge0  30694  nmoolb  30698  siii  30780  minvecolem2  30802  minvecolem4  30807  minvecolem5  30808  hlipgt0  30841  normge0  31053  normpyc  31073  pjhthlem1  31318  pjige0i  31617  nmoplb  31834  nmfnlb  31851  branmfn  32032  pjssdif2i  32101  stlei  32167  xlt2addrd  32682  eliccelico  32700  elicoelioo  32701  bcm1n  32718  fsumiunle  32754  sgnmul  32760  nexple  32769  expevenpos  32771  ccatdmss  32871  pfxlsw2ccat  32872  wrdt2ind  32875  chnub  32938  xrge0tsmsd  33002  gsumwrd2dccatlem  33006  omndmul2  33026  psgnfzto1stlem  33057  cycpmco2lem4  33086  cycpmco2lem5  33087  cyc3conja  33114  archirngz  33133  archiabllem2c  33139  ofldchr  33282  rprmasso2  33487  rprmirred  33492  1arithufdlem3  33507  lbslelsp  33583  fedgmullem2  33616  extdggt0  33645  evls1fldgencl  33657  fldextrspunlem1  33662  algextdeglem8  33704  rtelextdg2lem  33706  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  madjusmdetlem2  33805  locfinreflem  33817  xrge0iifiso  33912  gsumesum  34036  esumcst  34040  esumpcvgval  34055  esumcvg  34063  esumiun  34071  measssd  34192  measunl  34193  omssubadd  34278  carsgclctunlem3  34298  pmeasmono  34302  sibfof  34318  oddpwdc  34332  eulerpartlemgc  34340  iwrdsplit  34365  ballotlemsgt1  34489  ballotlemsel1i  34491  signsply0  34529  signstfvc  34552  signsvtp  34561  signsvfpn  34563  fdvposlt  34577  fdvneggt  34578  fdvnegge  34580  logdivsqrle  34628  hgt750lemf  34631  tgoldbachgtde  34638  swrdwlk  35095  subfaclim  35156  erdszelem7  35165  erdszelem8  35166  cvmliftlem2  35254  snmlff  35297  sinccvglem  35640  climlec3  35697  faclim  35709  fnejoin1  36332  poimirlem12  37602  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem23  37613  poimirlem28  37618  broucube  37624  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem  37641  itg2addnclem3  37643  itg2gt0cn  37645  itggt0cn  37660  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  isbnd3  37754  ssbnd  37758  heiborlem8  37788  bfplem2  37793  rrncmslem  37802  rrnequiv  37805  rrntotbnd  37806  lcv1  39005  lsatcv0eq  39011  lsatcvat3  39016  cvlsupr2  39307  hlatlej2  39340  cvrval4N  39379  cvratlem  39386  atcvr0eq  39391  2atlt  39404  atbtwnex  39413  athgt  39421  1cvrat  39441  ps-1  39442  hlatexch3N  39445  hlatexch4  39446  3atlem2  39449  atcvrlln2  39484  lplnexllnN  39529  4atlem3a  39562  4atlem10b  39570  4atlem11b  39573  4atlem12b  39576  2lplnja  39584  dalemply  39619  dalemsly  39620  dalem1  39624  dalem6  39633  dalem7  39634  dalem-cly  39636  dalem11  39639  dalem12  39640  dalem16  39644  dalem17  39645  dalem38  39675  dalem44  39681  dalem61  39698  lnatexN  39744  lncvrat  39747  lncmp  39748  paddasslem2  39786  dalawlem3  39838  dalawlem6  39841  dalawlem11  39846  lhpmcvr  39988  lhp2atne  39999  lhp2at0ne  40001  lautj  40058  trlval4  40153  cdlemc2  40157  cdlemc5  40160  cdleme3b  40194  cdleme11c  40226  cdleme19a  40268  cdleme20j  40283  cdleme22f  40311  cdleme23c  40316  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme35fnpq  40414  cdleme48bw  40467  cdlemg10a  40605  cdlemg11b  40607  cdlemg17g  40632  cdlemg18c  40645  cdlemi1  40783  cdlemk52  40919  dia2dimlem1  41029  dihord1  41183  dihjatcclem4  41386  lcmineqlem15  42002  lcmineqlem19  42006  lcmineqlem22  42009  aks4d1lem1  42021  aks4d1p1p4  42030  aks4d1p1p5  42034  aks4d1p2  42036  aks4d1p3  42037  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  aks6d1c1p6  42073  aks6d1c1  42075  aks6d1c2  42089  sticksstones7  42111  aks6d1c7lem1  42139  unitscyglem4  42157  metakunt7  42170  metakunt15  42178  metakunt16  42179  2xp3dxp2ge1d  42200  dvdsexpnn0  42330  prjspner01  42595  flt4lem5  42620  fltnltalem  42632  fltnlta  42633  3cubeslem1  42654  eldioph2lem1  42730  lzenom  42740  irrapxlem1  42792  irrapxlem4  42795  irrapxlem5  42796  pell14qrgt0  42829  pell1qrge1  42840  pell1qrgap  42844  pellfundge  42852  pellfundex  42856  pellfund14  42868  rmspecsqrtnq  42876  rmxypos  42918  ltrmynn0  42919  ltrmxnn0  42920  jm2.24nn  42930  jm2.17b  42932  jm2.17c  42933  jm2.24  42934  congadd  42937  congsym  42939  congneg  42940  congid  42942  mzpcong  42943  acongrep  42951  acongeq  42954  jm2.18  42959  jm2.19  42964  jm2.23  42967  jm2.25  42970  jm2.26lem3  42972  jm2.15nn0  42974  jm2.16nn0  42975  jm2.27a  42976  jm2.27c  42978  jm3.1lem1  42988  idomsubgmo  43164  sqrtcval  43612  inductionexd  44126  imo72b2lem0  44136  imo72b2  44143  dvgrat  44284  radcnvrat  44286  binomcxplemnn0  44321  binomcxplemnotnn0  44328  cncmpmax  45004  rnmptlb  45215  zltlesub  45262  infxrpnf  45421  xrpnf  45460  fmul01  45557  fmul01lt1lem1  45561  climdivf  45589  sumnnodd  45607  climinf2lem  45683  limsup10exlem  45749  climliminf  45783  dfxlim2v  45824  xlimliminflimsup  45839  dvdivbd  45900  volge0  45938  stoweidlem1  45978  stoweidlem16  45993  stoweidlem18  45995  stoweidlem24  46001  stoweidlem26  46003  stoweidlem36  46013  stoweidlem38  46015  stoweidlem41  46018  stoweidlem42  46019  stoweidlem44  46021  stoweidlem45  46022  stoweidlem48  46025  stoweidlem62  46039  wallispilem5  46046  stirlinglem1  46051  stirlinglem5  46055  stirlinglem7  46057  stirlinglem8  46058  stirlinglem9  46059  stirlinglem11  46061  fourierdlem4  46088  fourierdlem10  46094  fourierdlem37  46121  fourierdlem47  46130  fourierdlem72  46155  fourierdlem74  46157  fourierdlem79  46162  fourierdlem82  46165  fourierdlem89  46172  fourierdlem91  46174  fourierdlem93  46176  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  etransclem24  46235  etransclem25  46236  etransclem28  46239  etransclem37  46248  etransclem38  46249  etransclem44  46255  meaiuninc3v  46461  vonicclem1  46660  pimconstlt0  46678  smfsuplem1  46788  rlimdmafv  47154  rlimdmafv2  47235  2elfz2melfz  47295  iccpartgtprec  47382  iccpartlt  47386  iccpartgtl  47388  sqrtpwpw2p  47500  fmtnodvds  47506  goldbachthlem1  47507  lighneallem4a  47570  perfectALTVlem1  47683  uhgrimgrlim  47947  cznnring  48185  altgsumbcALT  48276  expnegico01  48442  flnn0div2ge  48461  rege1logbrege0  48486  fllogbd  48488  nnpw2blen  48508  nnolog2flm1  48518  dignn0ldlem  48530  dignn0flhalflem1  48543  dignn0flhalflem2  48544  eenglngeehlnmlem2  48666  itsclc0yqsol  48692  2itscp  48709  itscnhlinecirc02plem1  48710  itscnhlinecirc02plem2  48711  inlinecirc02p  48715