Theorem breqtrrd 5135

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  marypha1lem  9384  marypha2  9390  infsupprpr  9457  unxpwdom  9542  ttrcltr  9669  onadju  10147  nnadju  10151  cfss  10218  tskuni  10736  ltexnq  10928  lt2addmuld  12432  div4p1lem1div2  12437  nn0le2x  12496  mul2lt0rgt0  13056  prodge0ld  13061  ge2halflem1  13068  xrmax1  13135  xrmax2  13136  max1ALT  13146  qbtwnxr  13160  xleadd1a  13213  xlt2add  13220  xlesubadd  13223  xmulgt0  13243  xlemul1a  13248  xov1plusxeqvd  13459  uzsubsubfz  13507  fzctr  13601  subfzo0  13750  flflp1  13769  fldiv4lem1div2uz2  13798  ceilge  13807  modge0  13841  modlt  13842  modid  13858  m1modge3gt1  13883  modaddmodup  13899  sermono  13999  seqf1olem1  14006  seqf1olem2  14007  sqgt0  14091  sqge0  14101  leexp1a  14140  nnlesq  14170  expnbnd  14197  expmulnbnd  14200  discr1  14204  facwordi  14254  faclbnd5  14263  nfile  14324  hashdom  14344  hashgt23el  14389  fi1uzind  14472  brfi1indALT  14475  ccatws1n0  14597  swrds2  14906  cjmulge0  15112  resqrtcl  15219  absge0  15253  sqreulem  15326  amgm2  15336  rlimdm  15517  rlimge0  15547  reccn2  15563  climle  15606  climserle  15629  isercoll2  15635  iseraltlem1  15648  iseralt  15651  isumclim2  15724  isumclim3  15725  isumge0  15732  fsumless  15762  cvgcmp  15782  cvgcmpce  15784  abscvgcvg  15785  isumsup2  15812  isumltss  15814  climcndslem1  15815  climcnds  15817  supcvg  15822  harmonic  15825  expcnv  15830  explecnv  15831  cvgrat  15849  mertenslem1  15850  mertenslem2  15851  clim2div  15855  ntrivcvgtail  15866  iprodclim2  15965  iprodclim3  15966  efcvg  16051  ege2le3  16056  efaddlem  16059  eftlub  16077  effsumlt  16079  tanhlt1  16128  ef01bndlem  16152  sin02gt0  16160  rpnnen2lem4  16185  ruclem2  16200  ruclem3  16201  ruclem9  16206  iddvdsexp  16249  dvdsadd  16272  dvdsfac  16296  dvdsexp2im  16297  dvdsmod  16299  3dvds  16301  omoe  16334  sumeven  16357  divalglem1  16364  flodddiv4t2lthalf  16388  bitsfzo  16405  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  sadcaddlem  16427  sadadd3  16431  sadaddlem  16436  dvdssqim  16524  dvdsexpim  16525  dvdsmulgcd  16526  nn0seqcvgd  16540  dvdslcm  16568  lcmgcdlem  16576  dvdslcmf  16601  lcmfunsnlem2lem2  16609  mulgcddvds  16625  qredeq  16627  cncongr2  16638  sqnprm  16672  isprm6  16684  dvdszzq  16691  prmdvdsbc  16696  nonsq  16729  hashdvds  16745  prmdiv  16755  odzdvds  16766  pythagtriplem4  16790  pcpre1  16813  pcdvdsb  16840  pcz  16852  pcprmpw2  16853  pcaddlem  16859  pcadd  16860  pcadd2  16861  pcmpt  16863  pcmptdvds  16865  fldivp1  16868  pcfaclem  16869  pockthlem  16876  prmreclem1  16887  prmreclem3  16889  prmreclem5  16891  prmreclem6  16892  4sqlem6  16914  4sqlem8  16916  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  4sqlem16  16931  vdwlem3  16954  vdwlem9  16960  vdwlem10  16961  vdwlem12  16963  ramub1lem2  16998  prmgap  17030  prmgaplcm  17031  prmgapprmo  17033  mreexexd  17609  invfuc  17939  ple1  18389  eqgen  19113  lagsubg  19127  pgpfi  19535  sylow2alem2  19548  sylow2a  19549  sylow3lem4  19560  efgsrel  19664  odadd1  19778  odadd2  19779  gexex  19783  lt6abl  19825  dprd2d2  19976  dmdprdpr  19981  ablfacrp2  19999  ablfac1c  20003  pgpfaclem1  20013  ablfac2  20021  fincygsubgodd  20044  dvdsrmul1  20278  unitmulclb  20290  subrguss  20496  rhmsubcrngc  20577  abvres  20740  znfld  21470  znunit  21473  frlmisfrlm  21757  ply1coefsupp  22184  evl1gsumadd  22245  matgsum  22324  pm2mpcl  22684  psmetxrge0  24201  isxmet2d  24215  mettri  24240  xmettri3  24241  mettri3  24242  xmetrtri2  24244  prdsxmetlem  24256  imasdsf1olem  24261  xblss2ps  24289  blss2ps  24291  blss2  24292  blssps  24312  blss  24313  prdsbl  24379  dscmet  24460  nmge0  24505  nmmtri  24510  tngngp3  24544  nlmvscnlem2  24573  nrginvrcnlem  24579  nmoix  24617  nmoleub  24619  blcvx  24686  xrsxmet  24698  opnreen  24720  xrge0tsms  24723  icopnfcnv  24840  xrhmeo  24844  lebnumii  24865  pcophtb  24929  pi1grplem  24949  nmoleub2lem  25014  ipcau2  25134  tcphcphlem1  25135  ipcau  25138  ipcnlem2  25144  rrxcph  25292  minveclem2  25326  minveclem3b  25328  pjthlem1  25337  pjthlem2  25338  ivthlem3  25354  ivth2  25356  ovolfsf  25372  ovolsslem  25385  ovollb2lem  25389  ovollb2  25390  ovolctb  25391  ovolfiniun  25402  ovolicc1  25417  ovolicc2lem4  25421  ovolicc2  25423  nulmbl2  25437  unmbl  25438  ioombl1lem4  25462  uniioombllem4  25487  uniioombllem6  25489  volivth  25508  vitalilem4  25512  itg1ge0  25587  itg1ge0a  25612  itg1lea  25613  itg1climres  25615  mbfi1fseqlem5  25620  itg2ub  25634  itg2seq  25643  itg2uba  25644  itg2splitlem  25649  itg2split  25650  itg2monolem3  25653  itg2mono  25654  itg2i1fseq2  25657  itg2addlem  25659  iblss  25706  itggt0  25745  dvferm2lem  25890  dvlip  25898  dvivthlem1  25913  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  ftc1lem4  25946  ply1divmo  26041  ply1remlem  26070  fta1glem2  26074  idomrootle  26078  ig1pdvds  26085  plyeq0lem  26115  plydiveu  26206  fta1lem  26215  vieta1lem2  26219  aaliou3lem2  26251  aaliou3lem8  26253  ulmcn  26308  mtest  26313  itgulm  26317  radcnvlem1  26322  radcnvlt1  26327  dvradcnv  26330  pserdvlem2  26338  abelthlem2  26342  abelthlem6  26346  abelthlem7  26348  abelthlem9  26350  tangtx  26414  sinq12gt0  26416  sineq0  26433  cosordlem  26439  tanord  26447  tanregt0  26448  logrnaddcl  26483  logcj  26515  argregt0  26519  argrege0  26520  argimgt0  26521  argimlt0  26522  logimul  26523  logneg2  26524  logdivlti  26529  divlogrlim  26544  logcnlem3  26553  logcnlem4  26554  dvlog2lem  26561  logtayl  26569  rpcxpcl  26585  cxpsqrtlem  26611  cxpaddle  26662  isosctrlem1  26728  asinlem3a  26780  asinlem3  26781  asinneg  26796  asinsinlem  26801  asinsin  26802  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atanlogsub  26826  atantan  26833  atanbndlem  26835  atantayl  26847  leibpi  26852  birthdaylem3  26863  areaf  26871  cxploglim  26888  jensenlem2  26898  jensen  26899  logdiflbnd  26905  harmonicbnd4  26921  fsumharmonic  26922  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamcvg2  26965  wilthlem2  26979  wilthimp  26982  ftalem1  26983  ftalem2  26984  ftalem5  26987  basellem6  26996  basellem8  26998  basellem9  26999  chtge0  27022  chtublem  27122  logexprlim  27136  perfectlem1  27140  bcmax  27189  bposlem1  27195  bposlem2  27196  bposlem6  27200  bposlem7  27201  lgsdilem2  27244  lgsqrlem4  27260  lgsquadlem1  27291  2lgsoddprmlem2  27320  2sqlem3  27331  2sqlem8  27337  2sqblem  27342  2sqmod  27347  chebbnd1lem2  27381  chtppilimlem1  27384  chtppilim  27386  chto1ub  27387  vmadivsum  27393  rplogsumlem1  27395  rplogsumlem2  27396  dchrisum0lem1a  27397  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrvmasumlem2  27409  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem3  27430  dchrisum0  27431  mudivsum  27441  mulogsumlem  27442  mulog2sumlem1  27445  mulog2sumlem2  27446  2vmadivsumlem  27451  chpdifbndlem1  27464  selberg3lem1  27468  selberg4lem1  27471  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntibndlem3  27503  pntlemd  27505  pntlemc  27506  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemr  27513  pntlemf  27516  pntlemo  27518  abvcxp  27526  ostth2lem1  27529  padicabv  27541  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth2  27548  ostth3  27549  nodense  27604  nogt01o  27608  nosupbnd2lem1  27627  noetasuplem3  27647  maxs1  27677  maxs2  27678  cofcutr  27832  cofcutrtime  27835  addsuniflem  27908  negsunif  27961  ssltmul2  28051  precsexlem11  28119  abssge0  28147  sleabs  28150  onscutlt  28165  om2noseqlt  28193  expsgt0  28322  halfcut  28333  addhalfcut  28334  tgcgr4  28458  legso  28526  krippenlem  28617  midex  28664  oppperpex  28680  ttgcontlem1  28812  axpaschlem  28867  axcontlem8  28898  upgrex  29019  nbfusgrlevtxm1  29304  finsumvtxdgeven  29480  wwlksnextproplem3  29841  clwlkclwwlk2  29932  clwlkclwwlkfolem  29936  clwwlkndivn  30009  ex-ind-dvds  30390  nvabs  30601  nmooge0  30696  nmoolb  30700  siii  30782  minvecolem2  30804  minvecolem4  30809  minvecolem5  30810  hlipgt0  30843  normge0  31055  normpyc  31075  pjhthlem1  31320  pjige0i  31619  nmoplb  31836  nmfnlb  31853  branmfn  32034  pjssdif2i  32103  stlei  32169  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  33143  archiabllem2c  33149  ofldchr  33292  rprmasso2  33497  rprmirred  33502  1arithufdlem3  33517  lbslelsp  33593  fedgmullem2  33626  extdggt0  33653  evls1fldgencl  33665  fldextrspunlem1  33670  algextdeglem8  33714  rtelextdg2lem  33716  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  madjusmdetlem2  33818  locfinreflem  33830  xrge0iifiso  33925  gsumesum  34049  esumcst  34053  esumpcvgval  34068  esumcvg  34076  esumiun  34084  measssd  34205  measunl  34206  omssubadd  34291  carsgclctunlem3  34311  pmeasmono  34315  sibfof  34331  oddpwdc  34345  eulerpartlemgc  34353  iwrdsplit  34378  ballotlemsgt1  34502  ballotlemsel1i  34504  signsply0  34542  signstfvc  34565  signsvtp  34574  signsvfpn  34576  fdvposlt  34590  fdvneggt  34591  fdvnegge  34593  logdivsqrle  34641  hgt750lemf  34644  tgoldbachgtde  34651  swrdwlk  35114  subfaclim  35175  erdszelem7  35184  erdszelem8  35185  cvmliftlem2  35273  snmlff  35316  sinccvglem  35659  climlec3  35721  faclim  35733  fnejoin1  36356  poimirlem12  37626  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem28  37642  broucube  37648  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnclem3  37667  itg2gt0cn  37669  itggt0cn  37684  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  isbnd3  37778  ssbnd  37782  heiborlem8  37812  bfplem2  37817  rrncmslem  37826  rrnequiv  37829  rrntotbnd  37830  lcv1  39034  lsatcv0eq  39040  lsatcvat3  39045  cvlsupr2  39336  hlatlej2  39369  cvrval4N  39408  cvratlem  39415  atcvr0eq  39420  2atlt  39433  atbtwnex  39442  athgt  39450  1cvrat  39470  ps-1  39471  hlatexch3N  39474  hlatexch4  39475  3atlem2  39478  atcvrlln2  39513  lplnexllnN  39558  4atlem3a  39591  4atlem10b  39599  4atlem11b  39602  4atlem12b  39605  2lplnja  39613  dalemply  39648  dalemsly  39649  dalem1  39653  dalem6  39662  dalem7  39663  dalem-cly  39665  dalem11  39668  dalem12  39669  dalem16  39673  dalem17  39674  dalem38  39704  dalem44  39710  dalem61  39727  lnatexN  39773  lncvrat  39776  lncmp  39777  paddasslem2  39815  dalawlem3  39867  dalawlem6  39870  dalawlem11  39875  lhpmcvr  40017  lhp2atne  40028  lhp2at0ne  40030  lautj  40087  trlval4  40182  cdlemc2  40186  cdlemc5  40189  cdleme3b  40223  cdleme11c  40255  cdleme19a  40297  cdleme20j  40312  cdleme22f  40340  cdleme23c  40345  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme35fnpq  40443  cdleme48bw  40496  cdlemg10a  40634  cdlemg11b  40636  cdlemg17g  40661  cdlemg18c  40674  cdlemi1  40812  cdlemk52  40948  dia2dimlem1  41058  dihord1  41212  dihjatcclem4  41415  lcmineqlem15  42031  lcmineqlem19  42035  lcmineqlem22  42038  aks4d1lem1  42050  aks4d1p1p4  42059  aks4d1p1p5  42063  aks4d1p2  42065  aks4d1p3  42066  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  aks6d1c1p6  42102  aks6d1c1  42104  aks6d1c2  42118  sticksstones7  42140  aks6d1c7lem1  42168  unitscyglem4  42186  dvdsexpnn0  42322  prjspner01  42613  flt4lem5  42638  fltnltalem  42650  fltnlta  42651  3cubeslem1  42672  eldioph2lem1  42748  lzenom  42758  irrapxlem1  42810  irrapxlem4  42813  irrapxlem5  42814  pell14qrgt0  42847  pell1qrge1  42858  pell1qrgap  42862  pellfundge  42870  pellfundex  42874  pellfund14  42886  rmspecsqrtnq  42894  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  jm2.24nn  42948  jm2.17b  42950  jm2.17c  42951  jm2.24  42952  congadd  42955  congsym  42957  congneg  42958  congid  42960  mzpcong  42961  acongrep  42969  acongeq  42972  jm2.18  42977  jm2.19  42982  jm2.23  42985  jm2.25  42988  jm2.26lem3  42990  jm2.15nn0  42992  jm2.16nn0  42993  jm2.27a  42994  jm2.27c  42996  jm3.1lem1  43006  idomsubgmo  43182  sqrtcval  43630  inductionexd  44144  imo72b2lem0  44154  imo72b2  44161  dvgrat  44301  radcnvrat  44303  binomcxplemnn0  44338  binomcxplemnotnn0  44345  cncmpmax  45026  rnmptlb  45237  zltlesub  45283  infxrpnf  45442  xrpnf  45481  fmul01  45578  fmul01lt1lem1  45582  climdivf  45610  sumnnodd  45628  climinf2lem  45704  limsup10exlem  45770  climliminf  45804  dfxlim2v  45845  xlimliminflimsup  45860  dvdivbd  45921  volge0  45959  stoweidlem1  45999  stoweidlem16  46014  stoweidlem18  46016  stoweidlem24  46022  stoweidlem26  46024  stoweidlem36  46034  stoweidlem38  46036  stoweidlem41  46039  stoweidlem42  46040  stoweidlem44  46042  stoweidlem45  46043  stoweidlem48  46046  stoweidlem62  46060  wallispilem5  46067  stirlinglem1  46072  stirlinglem5  46076  stirlinglem7  46078  stirlinglem8  46079  stirlinglem9  46080  stirlinglem11  46082  fourierdlem4  46109  fourierdlem10  46115  fourierdlem37  46142  fourierdlem47  46151  fourierdlem72  46176  fourierdlem74  46178  fourierdlem79  46183  fourierdlem82  46186  fourierdlem89  46193  fourierdlem91  46195  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  etransclem24  46256  etransclem25  46257  etransclem28  46260  etransclem37  46269  etransclem38  46270  etransclem44  46276  meaiuninc3v  46482  vonicclem1  46681  pimconstlt0  46699  smfsuplem1  46809  rlimdmafv  47178  rlimdmafv2  47259  2elfz2melfz  47319  iccpartgtprec  47421  iccpartlt  47425  iccpartgtl  47427  sqrtpwpw2p  47539  fmtnodvds  47545  goldbachthlem1  47546  lighneallem4a  47609  perfectALTVlem1  47722  uhgrimgrlim  47986  cznnring  48250  altgsumbcALT  48341  expnegico01  48507  flnn0div2ge  48522  rege1logbrege0  48547  fllogbd  48549  nnpw2blen  48569  nnolog2flm1  48579  dignn0ldlem  48591  dignn0flhalflem1  48604  dignn0flhalflem2  48605  eenglngeehlnmlem2  48727  itsclc0yqsol  48753  2itscp  48770  itscnhlinecirc02plem1  48771  itscnhlinecirc02plem2  48772  inlinecirc02p  48776