Theorem breqtrrd 5176

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

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

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  marypha1lem  9432  marypha2  9438  infsupprpr  9503  unxpwdom  9588  ttrcltr  9715  onadju  10192  nnadju  10196  cfss  10264  tskuni  10782  ltexnq  10974  lt2addmuld  12467  div4p1lem1div2  12472  mul2lt0rgt0  13082  prodge0ld  13087  xrmax1  13159  xrmax2  13160  max1ALT  13170  qbtwnxr  13184  xleadd1a  13237  xlt2add  13244  xlesubadd  13247  xmulgt0  13267  xlemul1a  13272  xov1plusxeqvd  13480  uzsubsubfz  13528  fzctr  13618  subfzo0  13759  flflp1  13777  fldiv4lem1div2uz2  13806  ceilge  13815  modge0  13849  modlt  13850  modid  13866  m1modge3gt1  13888  modaddmodup  13904  sermono  14005  seqf1olem1  14012  seqf1olem2  14013  sqgt0  14096  sqge0  14106  leexp1a  14145  nnlesq  14174  expnbnd  14200  expmulnbnd  14203  discr1  14207  facwordi  14254  faclbnd5  14263  nfile  14324  hashdom  14344  hashgt23el  14389  fi1uzind  14463  brfi1indALT  14466  ccatws1n0  14587  swrds2  14896  cjmulge0  15098  resqrtcl  15205  absge0  15239  sqreulem  15311  amgm2  15321  rlimdm  15500  rlimge0  15530  reccn2  15546  climle  15589  climserle  15614  isercoll2  15620  iseraltlem1  15633  iseralt  15636  isumclim2  15709  isumclim3  15710  isumge0  15717  fsumless  15747  cvgcmp  15767  cvgcmpce  15769  abscvgcvg  15770  isumsup2  15797  isumltss  15799  climcndslem1  15800  climcnds  15802  supcvg  15807  harmonic  15810  expcnv  15815  explecnv  15816  cvgrat  15834  mertenslem1  15835  mertenslem2  15836  clim2div  15840  ntrivcvgtail  15851  iprodclim2  15948  iprodclim3  15949  efcvg  16033  ege2le3  16038  efaddlem  16041  eftlub  16057  effsumlt  16059  tanhlt1  16108  ef01bndlem  16132  sin02gt0  16140  rpnnen2lem4  16165  ruclem2  16180  ruclem3  16181  ruclem9  16186  iddvdsexp  16228  dvdsadd  16250  dvdsfac  16274  dvdsexp2im  16275  dvdsmod  16277  3dvds  16279  omoe  16312  sumeven  16335  divalglem1  16342  flodddiv4t2lthalf  16364  bitsfzo  16381  bitsmod  16382  bitscmp  16384  bitsinv1lem  16387  sadcaddlem  16403  sadadd3  16407  sadaddlem  16412  dvdssqim  16501  dvdsmulgcd  16502  nn0seqcvgd  16512  dvdslcm  16540  lcmgcdlem  16548  dvdslcmf  16573  lcmfunsnlem2lem2  16581  mulgcddvds  16597  qredeq  16599  cncongr2  16610  sqnprm  16644  isprm6  16656  nonsq  16700  hashdvds  16713  prmdiv  16723  odzdvds  16733  pythagtriplem4  16757  pcpre1  16780  pcdvdsb  16807  pcz  16819  pcprmpw2  16820  pcaddlem  16826  pcadd  16827  pcadd2  16828  pcmpt  16830  pcmptdvds  16832  fldivp1  16835  pcfaclem  16836  pockthlem  16843  prmreclem1  16854  prmreclem3  16856  prmreclem5  16858  prmreclem6  16859  4sqlem6  16881  4sqlem8  16883  4sqlem11  16893  4sqlem12  16894  4sqlem14  16896  4sqlem16  16898  vdwlem3  16921  vdwlem9  16927  vdwlem10  16928  vdwlem12  16930  ramub1lem2  16965  prmgap  16997  prmgaplcm  16998  prmgapprmo  17000  mreexexd  17597  invfuc  17932  ple1  18388  eqgen  19098  lagsubg  19111  pgpfi  19515  sylow2alem2  19528  sylow2a  19529  sylow3lem4  19540  efgsrel  19644  odadd1  19758  odadd2  19759  gexex  19763  lt6abl  19805  dprd2d2  19956  dmdprdpr  19961  ablfacrp2  19979  ablfac1c  19983  pgpfaclem1  19993  ablfac2  20001  fincygsubgodd  20024  dvdsrmul1  20261  unitmulclb  20273  subrguss  20478  abvres  20591  znfld  21336  znunit  21339  frlmisfrlm  21623  ply1coefsupp  22040  evl1gsumadd  22098  matgsum  22160  pm2mpcl  22520  psmetxrge0  24040  isxmet2d  24054  mettri  24079  xmettri3  24080  mettri3  24081  xmetrtri2  24083  prdsxmetlem  24095  imasdsf1olem  24100  xblss2ps  24128  blss2ps  24130  blss2  24131  blssps  24151  blss  24152  prdsbl  24221  dscmet  24302  nmge0  24347  nmmtri  24352  tngngp3  24394  nlmvscnlem2  24423  nrginvrcnlem  24429  nmoix  24467  nmoleub  24469  blcvx  24535  xrsxmet  24546  opnreen  24568  xrge0tsms  24571  icopnfcnv  24688  xrhmeo  24692  lebnumii  24713  pcophtb  24777  pi1grplem  24797  nmoleub2lem  24862  ipcau2  24983  tcphcphlem1  24984  ipcau  24987  ipcnlem2  24993  rrxcph  25141  minveclem2  25175  minveclem3b  25177  pjthlem1  25186  pjthlem2  25187  ivthlem3  25203  ivth2  25205  ovolfsf  25221  ovolsslem  25234  ovollb2lem  25238  ovollb2  25239  ovolctb  25240  ovolfiniun  25251  ovolicc1  25266  ovolicc2lem4  25270  ovolicc2  25272  nulmbl2  25286  unmbl  25287  ioombl1lem4  25311  uniioombllem4  25336  uniioombllem6  25338  volivth  25357  vitalilem4  25361  itg1ge0  25436  itg1ge0a  25462  itg1lea  25463  itg1climres  25465  mbfi1fseqlem5  25470  itg2ub  25484  itg2seq  25493  itg2uba  25494  itg2splitlem  25499  itg2split  25500  itg2monolem3  25503  itg2mono  25504  itg2i1fseq2  25507  itg2addlem  25509  iblss  25555  itggt0  25594  dvferm2lem  25739  dvlip  25746  dvivthlem1  25761  dvfsumlem2  25780  dvfsumlem3  25781  ftc1lem4  25792  ply1divmo  25889  ply1remlem  25916  fta1glem2  25920  ig1pdvds  25930  plyeq0lem  25960  plydiveu  26048  fta1lem  26057  vieta1lem2  26061  aaliou3lem2  26093  aaliou3lem8  26095  ulmcn  26148  mtest  26153  itgulm  26157  radcnvlem1  26162  radcnvlt1  26167  dvradcnv  26170  pserdvlem2  26177  abelthlem2  26181  abelthlem6  26185  abelthlem7  26187  abelthlem9  26189  tangtx  26252  sinq12gt0  26254  sineq0  26270  cosordlem  26276  tanord  26284  tanregt0  26285  logrnaddcl  26320  logcj  26351  argregt0  26355  argrege0  26356  argimgt0  26357  argimlt0  26358  logimul  26359  logneg2  26360  logdivlti  26365  divlogrlim  26380  logcnlem3  26389  logcnlem4  26390  dvlog2lem  26397  logtayl  26405  rpcxpcl  26421  cxpsqrtlem  26447  cxpaddle  26497  isosctrlem1  26560  asinlem3a  26612  asinlem3  26613  asinneg  26628  asinsinlem  26633  asinsin  26634  atanlogaddlem  26655  atanlogadd  26656  atanlogsublem  26657  atanlogsub  26658  atantan  26665  atanbndlem  26667  atantayl  26679  leibpi  26684  birthdaylem3  26695  areaf  26703  cxploglim  26719  jensenlem2  26729  jensen  26730  logdiflbnd  26736  harmonicbnd4  26752  fsumharmonic  26753  zetacvg  26756  lgamgulmlem2  26771  lgamgulmlem3  26772  lgamcvg2  26796  wilthlem2  26810  wilthimp  26813  ftalem1  26814  ftalem2  26815  ftalem5  26818  basellem6  26827  basellem8  26829  basellem9  26830  chtge0  26853  chtublem  26951  logexprlim  26965  perfectlem1  26969  bcmax  27018  bposlem1  27024  bposlem2  27025  bposlem6  27029  bposlem7  27030  lgsdilem2  27073  lgsqrlem4  27089  lgsquadlem1  27120  2lgsoddprmlem2  27149  2sqlem3  27160  2sqlem8  27166  2sqblem  27171  2sqmod  27176  chebbnd1lem2  27210  chtppilimlem1  27213  chtppilim  27215  chto1ub  27216  vmadivsum  27222  rplogsumlem1  27224  rplogsumlem2  27225  dchrisum0lem1a  27226  rpvmasumlem  27227  dchrisumlem1  27229  dchrisumlem2  27230  dchrvmasumlem2  27238  dchrisum0flblem1  27248  dchrisum0flblem2  27249  dchrisum0lem1b  27255  dchrisum0lem1  27256  dchrisum0lem2a  27257  dchrisum0lem3  27259  dchrisum0  27260  mudivsum  27270  mulogsumlem  27271  mulog2sumlem1  27274  mulog2sumlem2  27275  2vmadivsumlem  27280  chpdifbndlem1  27293  selberg3lem1  27297  selberg4lem1  27300  pntrlog2bndlem1  27317  pntrlog2bndlem2  27318  pntrlog2bndlem3  27319  pntrlog2bndlem4  27320  pntpbnd1a  27325  pntpbnd1  27326  pntpbnd2  27327  pntibndlem2  27331  pntibndlem3  27332  pntlemd  27334  pntlemc  27335  pntlemb  27337  pntlemg  27338  pntlemh  27339  pntlemr  27342  pntlemf  27345  pntlemo  27347  abvcxp  27355  ostth2lem1  27358  padicabv  27370  ostth2lem2  27374  ostth2lem3  27375  ostth2lem4  27376  ostth2  27377  ostth3  27378  nodense  27432  nogt01o  27436  nosupbnd2lem1  27455  noetasuplem3  27475  maxs1  27505  maxs2  27506  cofcutr  27650  cofcutrtime  27653  addsuniflem  27724  negsunif  27769  ssltmul2  27843  precsexlem11  27903  tgcgr4  28050  legso  28118  krippenlem  28209  midex  28256  oppperpex  28272  ttgcontlem1  28410  axpaschlem  28466  axcontlem8  28497  upgrex  28620  nbfusgrlevtxm1  28902  finsumvtxdgeven  29077  wwlksnextproplem3  29433  clwlkclwwlk2  29524  clwlkclwwlkfolem  29528  clwwlkndivn  29601  ex-ind-dvds  29982  nvabs  30193  nmooge0  30288  nmoolb  30292  siii  30374  minvecolem2  30396  minvecolem4  30401  minvecolem5  30402  hlipgt0  30435  normge0  30647  normpyc  30667  pjhthlem1  30912  pjige0i  31211  nmoplb  31428  nmfnlb  31445  branmfn  31626  pjssdif2i  31695  stlei  31761  xlt2addrd  32239  eliccelico  32256  elicoelioo  32257  bcm1n  32274  dvdszzq  32289  prmdvdsbc  32290  fsumiunle  32303  pfxlsw2ccat  32384  wrdt2ind  32385  xrge0tsmsd  32480  omndmul2  32501  psgnfzto1stlem  32530  cycpmco2lem4  32559  cycpmco2lem5  32560  cyc3conja  32587  archirngz  32606  archiabllem2c  32612  ofldchr  32703  fedgmullem2  33004  extdggt0  33025  evls1fldgencl  33034  algextdeglem8  33070  madjusmdetlem2  33107  locfinreflem  33119  xrge0iifiso  33214  nexple  33306  gsumesum  33356  esumcst  33360  esumpcvgval  33375  esumcvg  33383  esumiun  33391  measssd  33512  measunl  33513  omssubadd  33598  carsgclctunlem3  33618  pmeasmono  33622  sibfof  33638  oddpwdc  33652  eulerpartlemgc  33660  iwrdsplit  33685  ballotlemsgt1  33808  ballotlemsel1i  33810  sgnmul  33840  signsply0  33861  signstfvc  33884  signsvtp  33893  signsvfpn  33895  fdvposlt  33910  fdvneggt  33911  fdvnegge  33913  logdivsqrle  33961  hgt750lemf  33964  tgoldbachgtde  33971  swrdwlk  34416  subfaclim  34478  erdszelem7  34487  erdszelem8  34488  cvmliftlem2  34576  snmlff  34619  sinccvglem  34956  climlec3  35008  faclim  35021  gg-dvfsumlem2  35470  fnejoin1  35557  poimirlem12  36804  poimirlem17  36809  poimirlem19  36811  poimirlem20  36812  poimirlem23  36815  poimirlem28  36820  broucube  36826  mblfinlem2  36830  mblfinlem3  36831  mblfinlem4  36832  ismblfin  36833  itg2addnclem  36843  itg2addnclem3  36845  itg2gt0cn  36847  itggt0cn  36862  ftc1anclem5  36869  ftc1anclem7  36871  ftc1anclem8  36872  isbnd3  36956  ssbnd  36960  heiborlem8  36990  bfplem2  36995  rrncmslem  37004  rrnequiv  37007  rrntotbnd  37008  lcv1  38215  lsatcv0eq  38221  lsatcvat3  38226  cvlsupr2  38517  hlatlej2  38550  cvrval4N  38589  cvratlem  38596  atcvr0eq  38601  2atlt  38614  atbtwnex  38623  athgt  38631  1cvrat  38651  ps-1  38652  hlatexch3N  38655  hlatexch4  38656  3atlem2  38659  atcvrlln2  38694  lplnexllnN  38739  4atlem3a  38772  4atlem10b  38780  4atlem11b  38783  4atlem12b  38786  2lplnja  38794  dalemply  38829  dalemsly  38830  dalem1  38834  dalem6  38843  dalem7  38844  dalem-cly  38846  dalem11  38849  dalem12  38850  dalem16  38854  dalem17  38855  dalem38  38885  dalem44  38891  dalem61  38908  lnatexN  38954  lncvrat  38957  lncmp  38958  paddasslem2  38996  dalawlem3  39048  dalawlem6  39051  dalawlem11  39056  lhpmcvr  39198  lhp2atne  39209  lhp2at0ne  39211  lautj  39268  trlval4  39363  cdlemc2  39367  cdlemc5  39370  cdleme3b  39404  cdleme11c  39436  cdleme19a  39478  cdleme20j  39493  cdleme22f  39521  cdleme23c  39526  cdleme26f2ALTN  39539  cdleme26f2  39540  cdleme35fnpq  39624  cdleme48bw  39677  cdlemg10a  39815  cdlemg11b  39817  cdlemg17g  39842  cdlemg18c  39855  cdlemi1  39993  cdlemk52  40129  dia2dimlem1  40239  dihord1  40393  dihjatcclem4  40596  lcmineqlem15  41215  lcmineqlem19  41219  lcmineqlem22  41222  aks4d1lem1  41234  aks4d1p1p4  41243  aks4d1p1p5  41247  aks4d1p2  41249  aks4d1p3  41250  aks4d1p6  41253  aks4d1p7d1  41254  aks4d1p7  41255  aks4d1p8  41259  aks4d1p9  41260  sticksstones7  41275  metakunt7  41298  metakunt15  41306  metakunt16  41307  2xp3dxp2ge1d  41329  dvdsexpim  41522  dvdsexpnn0  41535  prjspner01  41670  flt4lem5  41695  fltnltalem  41707  fltnlta  41708  3cubeslem1  41725  eldioph2lem1  41801  lzenom  41811  irrapxlem1  41863  irrapxlem4  41866  irrapxlem5  41867  pell14qrgt0  41900  pell1qrge1  41911  pell1qrgap  41915  pellfundge  41923  pellfundex  41927  pellfund14  41939  rmspecsqrtnq  41947  rmxypos  41989  ltrmynn0  41990  ltrmxnn0  41991  jm2.24nn  42001  jm2.17b  42003  jm2.17c  42004  jm2.24  42005  congadd  42008  congsym  42010  congneg  42011  congid  42013  mzpcong  42014  acongrep  42022  acongeq  42025  jm2.18  42030  jm2.19  42035  jm2.23  42038  jm2.25  42041  jm2.26lem3  42043  jm2.15nn0  42045  jm2.16nn0  42046  jm2.27a  42047  jm2.27c  42049  jm3.1lem1  42059  idomrootle  42240  idomsubgmo  42243  sqrtcval  42695  inductionexd  43209  imo72b2  43227  dvgrat  43374  radcnvrat  43376  binomcxplemnn0  43411  binomcxplemnotnn0  43418  cncmpmax  44019  rnmptlb  44246  zltlesub  44294  infxrpnf  44455  xrpnf  44495  fmul01  44595  fmul01lt1lem1  44599  climdivf  44627  sumnnodd  44645  climinf2lem  44721  limsup10exlem  44787  climliminf  44821  dfxlim2v  44862  xlimliminflimsup  44877  dvdivbd  44938  volge0  44976  stoweidlem1  45016  stoweidlem16  45031  stoweidlem18  45033  stoweidlem24  45039  stoweidlem26  45041  stoweidlem36  45051  stoweidlem38  45053  stoweidlem41  45056  stoweidlem42  45057  stoweidlem44  45059  stoweidlem45  45060  stoweidlem48  45063  stoweidlem62  45077  wallispilem5  45084  stirlinglem1  45089  stirlinglem5  45093  stirlinglem7  45095  stirlinglem8  45096  stirlinglem9  45097  stirlinglem11  45099  fourierdlem4  45126  fourierdlem10  45132  fourierdlem37  45159  fourierdlem47  45168  fourierdlem72  45193  fourierdlem74  45195  fourierdlem79  45200  fourierdlem82  45203  fourierdlem89  45210  fourierdlem91  45212  fourierdlem93  45214  fourierdlem103  45224  fourierdlem104  45225  fourierdlem112  45233  etransclem24  45273  etransclem25  45274  etransclem28  45277  etransclem37  45286  etransclem38  45287  etransclem44  45293  meaiuninc3v  45499  vonicclem1  45698  pimconstlt0  45716  smfsuplem1  45826  rlimdmafv  46184  rlimdmafv2  46265  2elfz2melfz  46325  iccpartgtprec  46387  iccpartlt  46391  iccpartgtl  46393  sqrtpwpw2p  46505  fmtnodvds  46511  goldbachthlem1  46512  lighneallem4a  46575  perfectALTVlem1  46688  cznnring  46943  rhmsubcrngc  47016  altgsumbcALT  47118  expnegico01  47287  flnn0div2ge  47307  rege1logbrege0  47332  fllogbd  47334  nnpw2blen  47354  nnolog2flm1  47364  dignn0ldlem  47376  dignn0flhalflem1  47389  dignn0flhalflem2  47390  eenglngeehlnmlem2  47512  itsclc0yqsol  47538  2itscp  47555  itscnhlinecirc02plem1  47556  itscnhlinecirc02plem2  47557  inlinecirc02p  47561