Theorem breqtrrd 5102

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075

This theorem is referenced by:  marypha1lem  9335  marypha2  9341  infsupprpr  9408  unxpwdom  9493  ttrcltr  9626  onadju  10105  nnadju  10109  cfss  10176  tskuni  10695  ltexnq  10887  lt2addmuld  12416  div4p1lem1div2  12421  nn0le2x  12480  mul2lt0rgt0  13036  prodge0ld  13041  ge2halflem1  13048  xrmax1  13116  xrmax2  13117  max1ALT  13127  qbtwnxr  13141  xleadd1a  13194  xlt2add  13201  xlesubadd  13204  xmulgt0  13224  xlemul1a  13229  xov1plusxeqvd  13440  uzsubsubfz  13489  fzctr  13583  subfzo0  13736  flflp1  13755  fldiv4lem1div2uz2  13784  ceilge  13793  modge0  13827  modlt  13828  modid  13844  m1modge3gt1  13869  modaddmodup  13885  sermono  13985  seqf1olem1  13992  seqf1olem2  13993  sqgt0  14077  sqge0  14087  leexp1a  14126  nnlesq  14156  expnbnd  14183  expmulnbnd  14186  discr1  14190  facwordi  14240  faclbnd5  14249  nfile  14310  hashdom  14330  hashgt23el  14375  fi1uzind  14458  brfi1indALT  14461  ccatdmss  14533  ccatws1n0  14584  swrds2  14891  cjmulge0  15097  resqrtcl  15204  absge0  15238  sqreulem  15311  amgm2  15321  rlimdm  15502  rlimge0  15532  reccn2  15548  climle  15591  climserle  15614  isercoll2  15620  iseraltlem1  15633  iseralt  15636  isumclim2  15709  isumclim3  15710  isumge0  15717  fsumless  15748  cvgcmp  15768  cvgcmpce  15770  abscvgcvg  15771  isumsup2  15800  isumltss  15802  climcndslem1  15803  climcnds  15805  supcvg  15810  harmonic  15813  expcnv  15818  explecnv  15819  cvgrat  15837  mertenslem1  15838  mertenslem2  15839  clim2div  15843  ntrivcvgtail  15854  iprodclim2  15953  iprodclim3  15954  efcvg  16039  ege2le3  16044  efaddlem  16047  eftlub  16065  effsumlt  16067  tanhlt1  16116  ef01bndlem  16140  sin02gt0  16148  rpnnen2lem4  16173  ruclem2  16188  ruclem3  16189  ruclem9  16194  iddvdsexp  16237  dvdsadd  16260  dvdsfac  16284  dvdsexp2im  16285  dvdsmod  16287  3dvds  16289  omoe  16322  sumeven  16345  divalglem1  16352  flodddiv4t2lthalf  16376  bitsfzo  16393  bitsmod  16394  bitscmp  16396  bitsinv1lem  16399  sadcaddlem  16415  sadadd3  16419  sadaddlem  16424  dvdssqim  16512  dvdsexpim  16513  dvdsmulgcd  16514  nn0seqcvgd  16528  dvdslcm  16556  lcmgcdlem  16564  dvdslcmf  16589  lcmfunsnlem2lem2  16597  mulgcddvds  16613  qredeq  16615  cncongr2  16626  sqnprm  16661  isprm6  16673  dvdszzq  16680  prmdvdsbc  16685  nonsq  16718  hashdvds  16734  prmdiv  16744  odzdvds  16755  pythagtriplem4  16779  pcpre1  16802  pcdvdsb  16829  pcz  16841  pcprmpw2  16842  pcaddlem  16848  pcadd  16849  pcadd2  16850  pcmpt  16852  pcmptdvds  16854  fldivp1  16857  pcfaclem  16858  pockthlem  16865  prmreclem1  16876  prmreclem3  16878  prmreclem5  16880  prmreclem6  16881  4sqlem6  16903  4sqlem8  16905  4sqlem11  16915  4sqlem12  16916  4sqlem14  16918  4sqlem16  16920  vdwlem3  16943  vdwlem9  16949  vdwlem10  16950  vdwlem12  16952  ramub1lem2  16987  prmgap  17019  prmgaplcm  17020  prmgapprmo  17022  mreexexd  17603  invfuc  17933  ple1  18383  chnub  18577  eqgen  19145  lagsubg  19159  pgpfi  19569  sylow2alem2  19582  sylow2a  19583  sylow3lem4  19594  efgsrel  19698  odadd1  19812  odadd2  19813  gexex  19817  lt6abl  19859  dprd2d2  20010  dmdprdpr  20015  ablfacrp2  20033  ablfac1c  20037  pgpfaclem1  20047  ablfac2  20055  fincygsubgodd  20078  omndmul2  20097  dvdsrmul1  20338  unitmulclb  20350  subrguss  20553  rhmsubcrngc  20634  abvres  20797  znfld  21529  znunit  21532  ofldchr  21545  frlmisfrlm  21817  ply1coefsupp  22250  evl1gsumadd  22311  matgsum  22390  pm2mpcl  22750  psmetxrge0  24266  isxmet2d  24280  mettri  24305  xmettri3  24306  mettri3  24307  xmetrtri2  24309  prdsxmetlem  24321  imasdsf1olem  24326  xblss2ps  24354  blss2ps  24356  blss2  24357  blssps  24377  blss  24378  prdsbl  24444  dscmet  24525  nmge0  24570  nmmtri  24575  tngngp3  24609  nlmvscnlem2  24638  nrginvrcnlem  24644  nmoix  24682  nmoleub  24684  blcvx  24751  xrsxmet  24763  opnreen  24785  xrge0tsms  24788  icopnfcnv  24897  xrhmeo  24901  lebnumii  24921  pcophtb  24984  pi1grplem  25004  nmoleub2lem  25069  ipcau2  25189  tcphcphlem1  25190  ipcau  25193  ipcnlem2  25199  rrxcph  25347  minveclem2  25381  minveclem3b  25383  pjthlem1  25392  pjthlem2  25393  ivthlem3  25408  ivth2  25410  ovolfsf  25426  ovolsslem  25439  ovollb2lem  25443  ovollb2  25444  ovolctb  25445  ovolfiniun  25456  ovolicc1  25471  ovolicc2lem4  25475  ovolicc2  25477  nulmbl2  25491  unmbl  25492  ioombl1lem4  25516  uniioombllem4  25541  uniioombllem6  25543  volivth  25562  vitalilem4  25566  itg1ge0  25641  itg1ge0a  25666  itg1lea  25667  itg1climres  25669  mbfi1fseqlem5  25674  itg2ub  25688  itg2seq  25697  itg2uba  25698  itg2splitlem  25703  itg2split  25704  itg2monolem3  25707  itg2mono  25708  itg2i1fseq2  25711  itg2addlem  25713  iblss  25760  itggt0  25799  dvferm2lem  25941  dvlip  25948  dvivthlem1  25963  dvfsumlem2  25982  dvfsumlem3  25983  ftc1lem4  25994  ply1divmo  26089  ply1remlem  26118  fta1glem2  26122  idomrootle  26126  ig1pdvds  26133  plyeq0lem  26163  plydiveu  26252  fta1lem  26261  vieta1lem2  26265  aaliou3lem2  26297  aaliou3lem8  26299  ulmcn  26352  mtest  26357  itgulm  26361  radcnvlem1  26366  radcnvlt1  26371  dvradcnv  26374  pserdvlem2  26381  abelthlem2  26385  abelthlem6  26389  abelthlem7  26391  abelthlem9  26393  tangtx  26457  sinq12gt0  26459  sineq0  26476  cosordlem  26482  tanord  26490  tanregt0  26491  logrnaddcl  26526  logcj  26558  argregt0  26562  argrege0  26563  argimgt0  26564  argimlt0  26565  logimul  26566  logneg2  26567  logdivlti  26572  divlogrlim  26587  logcnlem3  26596  logcnlem4  26597  dvlog2lem  26604  logtayl  26612  rpcxpcl  26628  cxpsqrtlem  26654  cxpaddle  26704  isosctrlem1  26770  asinlem3a  26822  asinlem3  26823  asinneg  26838  asinsinlem  26843  asinsin  26844  atanlogaddlem  26865  atanlogadd  26866  atanlogsublem  26867  atanlogsub  26868  atantan  26875  atanbndlem  26877  atantayl  26889  leibpi  26894  birthdaylem3  26905  areaf  26913  cxploglim  26929  jensenlem2  26939  jensen  26940  logdiflbnd  26946  harmonicbnd4  26962  fsumharmonic  26963  zetacvg  26966  lgamgulmlem2  26981  lgamgulmlem3  26982  lgamcvg2  27006  wilthlem2  27020  wilthimp  27023  ftalem1  27024  ftalem2  27025  ftalem5  27028  basellem6  27037  basellem8  27039  basellem9  27040  chtge0  27063  chtublem  27162  logexprlim  27176  perfectlem1  27180  bcmax  27229  bposlem1  27235  bposlem2  27236  bposlem6  27240  bposlem7  27241  lgsdilem2  27284  lgsqrlem4  27300  lgsquadlem1  27331  2lgsoddprmlem2  27360  2sqlem3  27371  2sqlem8  27377  2sqblem  27382  2sqmod  27387  chebbnd1lem2  27421  chtppilimlem1  27424  chtppilim  27426  chto1ub  27427  vmadivsum  27433  rplogsumlem1  27435  rplogsumlem2  27436  dchrisum0lem1a  27437  rpvmasumlem  27438  dchrisumlem1  27440  dchrisumlem2  27441  dchrvmasumlem2  27449  dchrisum0flblem1  27459  dchrisum0flblem2  27460  dchrisum0lem1b  27466  dchrisum0lem1  27467  dchrisum0lem2a  27468  dchrisum0lem3  27470  dchrisum0  27471  mudivsum  27481  mulogsumlem  27482  mulog2sumlem1  27485  mulog2sumlem2  27486  2vmadivsumlem  27491  chpdifbndlem1  27504  selberg3lem1  27508  selberg4lem1  27511  pntrlog2bndlem1  27528  pntrlog2bndlem2  27529  pntrlog2bndlem3  27530  pntrlog2bndlem4  27531  pntpbnd1a  27536  pntpbnd1  27537  pntpbnd2  27538  pntibndlem2  27542  pntibndlem3  27543  pntlemd  27545  pntlemc  27546  pntlemb  27548  pntlemg  27549  pntlemh  27550  pntlemr  27553  pntlemf  27556  pntlemo  27558  abvcxp  27566  ostth2lem1  27569  padicabv  27581  ostth2lem2  27585  ostth2lem3  27586  ostth2lem4  27587  ostth2  27588  ostth3  27589  nodense  27644  nogt01o  27648  nosupbnd2lem1  27667  noetasuplem3  27687  maxs1  27721  maxs2  27722  eqcuts3  27784  cofcutr  27904  cofcutrtime  27907  addsuniflem  27981  negsunif  28035  sltmuls2  28128  precsexlem11  28197  abssge0  28225  leabss  28228  oncutlt  28244  om2noseqlt  28279  zsoring  28389  expsgt0  28417  halfcut  28438  addhalfcut  28439  bdayfinbndlem1  28447  elreno2  28475  tgcgr4  28587  legso  28655  krippenlem  28746  midex  28793  oppperpex  28809  ttgcontlem1  28941  axpaschlem  28997  axcontlem8  29028  upgrex  29149  nbfusgrlevtxm1  29434  finsumvtxdgeven  29609  wwlksnextproplem3  29967  clwlkclwwlk2  30061  clwlkclwwlkfolem  30065  clwwlkndivn  30138  ex-ind-dvds  30519  nvabs  30731  nmooge0  30826  nmoolb  30830  siii  30912  minvecolem2  30934  minvecolem4  30939  minvecolem5  30940  hlipgt0  30973  normge0  31185  normpyc  31205  pjhthlem1  31450  pjige0i  31749  nmoplb  31966  nmfnlb  31983  branmfn  32164  pjssdif2i  32233  stlei  32299  xlt2addrd  32820  eliccelico  32838  elicoelioo  32839  bcm1n  32856  fsumiunle  32890  sgnmul  32896  nexple  32905  expevenpos  32907  pfxlsw2ccat  32998  wrdt2ind  33001  xrge0tsmsd  33122  gsumwrd2dccatlem  33126  psgnfzto1stlem  33149  cycpmco2lem4  33178  cycpmco2lem5  33179  cyc3conja  33206  archirngz  33238  archiabllem2c  33244  rprmasso2  33574  rprmirred  33579  1arithufdlem3  33594  vietadeg1  33710  lbslelsp  33730  fedgmullem2  33762  extdggt0  33789  evls1fldgencl  33802  fldextrspunlem1  33807  extdgfialglem1  33824  algextdeglem8  33856  rtelextdg2lem  33858  cos9thpiminplylem1  33914  cos9thpiminplylem2  33915  madjusmdetlem2  33960  locfinreflem  33972  xrge0iifiso  34067  gsumesum  34191  esumcst  34195  esumpcvgval  34210  esumcvg  34218  esumiun  34226  measssd  34347  measunl  34348  omssubadd  34432  carsgclctunlem3  34452  pmeasmono  34456  sibfof  34472  oddpwdc  34486  eulerpartlemgc  34494  iwrdsplit  34519  ballotlemsgt1  34643  ballotlemsel1i  34645  signsply0  34683  signstfvc  34706  signsvtp  34715  signsvfpn  34717  fdvposlt  34731  fdvneggt  34732  fdvnegge  34734  logdivsqrle  34782  hgt750lemf  34785  tgoldbachgtde  34792  swrdwlk  35297  subfaclim  35358  erdszelem7  35367  erdszelem8  35368  cvmliftlem2  35456  snmlff  35499  sinccvglem  35842  climlec3  35904  faclim  35916  fnejoin1  36538  poimirlem12  37941  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  poimirlem23  37952  poimirlem28  37957  broucube  37963  mblfinlem2  37967  mblfinlem3  37968  mblfinlem4  37969  ismblfin  37970  itg2addnclem  37980  itg2addnclem3  37982  itg2gt0cn  37984  itggt0cn  37999  ftc1anclem5  38006  ftc1anclem7  38008  ftc1anclem8  38009  isbnd3  38093  ssbnd  38097  heiborlem8  38127  bfplem2  38132  rrncmslem  38141  rrnequiv  38144  rrntotbnd  38145  lcv1  39475  lsatcv0eq  39481  lsatcvat3  39486  cvlsupr2  39777  hlatlej2  39810  cvrval4N  39848  cvratlem  39855  atcvr0eq  39860  2atlt  39873  atbtwnex  39882  athgt  39890  1cvrat  39910  ps-1  39911  hlatexch3N  39914  hlatexch4  39915  3atlem2  39918  atcvrlln2  39953  lplnexllnN  39998  4atlem3a  40031  4atlem10b  40039  4atlem11b  40042  4atlem12b  40045  2lplnja  40053  dalemply  40088  dalemsly  40089  dalem1  40093  dalem6  40102  dalem7  40103  dalem-cly  40105  dalem11  40108  dalem12  40109  dalem16  40113  dalem17  40114  dalem38  40144  dalem44  40150  dalem61  40167  lnatexN  40213  lncvrat  40216  lncmp  40217  paddasslem2  40255  dalawlem3  40307  dalawlem6  40310  dalawlem11  40315  lhpmcvr  40457  lhp2atne  40468  lhp2at0ne  40470  lautj  40527  trlval4  40622  cdlemc2  40626  cdlemc5  40629  cdleme3b  40663  cdleme11c  40695  cdleme19a  40737  cdleme20j  40752  cdleme22f  40780  cdleme23c  40785  cdleme26f2ALTN  40798  cdleme26f2  40799  cdleme35fnpq  40883  cdleme48bw  40936  cdlemg10a  41074  cdlemg11b  41076  cdlemg17g  41101  cdlemg18c  41114  cdlemi1  41252  cdlemk52  41388  dia2dimlem1  41498  dihord1  41652  dihjatcclem4  41855  lcmineqlem15  42470  lcmineqlem19  42474  lcmineqlem22  42477  aks4d1lem1  42489  aks4d1p1p4  42498  aks4d1p1p5  42502  aks4d1p2  42504  aks4d1p3  42505  aks4d1p6  42508  aks4d1p7d1  42509  aks4d1p7  42510  aks4d1p8  42514  aks4d1p9  42515  aks6d1c1p6  42541  aks6d1c1  42543  aks6d1c2  42557  sticksstones7  42579  aks6d1c7lem1  42607  unitscyglem4  42625  dvdsexpnn0  42754  prjspner01  43046  flt4lem5  43071  fltnltalem  43083  fltnlta  43084  3cubeslem1  43104  eldioph2lem1  43180  lzenom  43190  irrapxlem1  43238  irrapxlem4  43241  irrapxlem5  43242  pell14qrgt0  43275  pell1qrge1  43286  pell1qrgap  43290  pellfundge  43298  pellfundex  43302  pellfund14  43314  rmspecsqrtnq  43322  rmxypos  43363  ltrmynn0  43364  ltrmxnn0  43365  jm2.24nn  43375  jm2.17b  43377  jm2.17c  43378  jm2.24  43379  congadd  43382  congsym  43384  congneg  43385  congid  43387  mzpcong  43388  acongrep  43396  acongeq  43399  jm2.18  43404  jm2.19  43409  jm2.23  43412  jm2.25  43415  jm2.26lem3  43417  jm2.15nn0  43419  jm2.16nn0  43420  jm2.27a  43421  jm2.27c  43423  jm3.1lem1  43433  idomsubgmo  43609  sqrtcval  44056  inductionexd  44570  imo72b2lem0  44580  imo72b2  44587  dvgrat  44727  radcnvrat  44729  binomcxplemnn0  44764  binomcxplemnotnn0  44771  cncmpmax  45451  rnmptlb  45660  zltlesub  45706  infxrpnf  45862  xrpnf  45901  fmul01  45998  fmul01lt1lem1  46002  climdivf  46030  sumnnodd  46048  climinf2lem  46122  limsup10exlem  46188  climliminf  46222  dfxlim2v  46263  xlimliminflimsup  46278  dvdivbd  46339  volge0  46377  stoweidlem1  46417  stoweidlem16  46432  stoweidlem18  46434  stoweidlem24  46440  stoweidlem26  46442  stoweidlem36  46452  stoweidlem38  46454  stoweidlem41  46457  stoweidlem42  46458  stoweidlem44  46460  stoweidlem45  46461  stoweidlem48  46464  stoweidlem62  46478  wallispilem5  46485  stirlinglem1  46490  stirlinglem5  46494  stirlinglem7  46496  stirlinglem8  46497  stirlinglem9  46498  stirlinglem11  46500  fourierdlem4  46527  fourierdlem10  46533  fourierdlem37  46560  fourierdlem47  46569  fourierdlem72  46594  fourierdlem74  46596  fourierdlem79  46601  fourierdlem82  46604  fourierdlem89  46611  fourierdlem91  46613  fourierdlem93  46615  fourierdlem103  46625  fourierdlem104  46626  fourierdlem112  46634  etransclem24  46674  etransclem25  46675  etransclem28  46678  etransclem37  46687  etransclem38  46688  etransclem44  46694  meaiuninc3v  46900  vonicclem1  47099  pimconstlt0  47117  smfsuplem1  47227  chnerlem1  47300  rlimdmafv  47613  rlimdmafv2  47694  2elfz2melfz  47754  2timesltsq  47814  muldvdsfacgt  47822  iccpartgtprec  47868  iccpartlt  47872  iccpartgtl  47874  sqrtpwpw2p  47989  fmtnodvds  47995  goldbachthlem1  47996  lighneallem4a  48059  nprmdvdsfacm1lem1  48071  perfectALTVlem1  48185  uhgrimgrlim  48451  cznnring  48726  altgsumbcALT  48817  expnegico01  48982  flnn0div2ge  48997  rege1logbrege0  49022  fllogbd  49024  nnpw2blen  49044  nnolog2flm1  49054  dignn0ldlem  49066  dignn0flhalflem1  49079  dignn0flhalflem2  49080  eenglngeehlnmlem2  49202  itsclc0yqsol  49228  2itscp  49245  itscnhlinecirc02plem1  49246  itscnhlinecirc02plem2  49247  inlinecirc02p  49251