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

Syntax hints:   → wi 4   = wceq 1541   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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  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  9430  marypha2  9436  infsupprpr  9501  unxpwdom  9586  ttrcltr  9713  onadju  10190  nnadju  10194  cfss  10262  tskuni  10780  ltexnq  10972  lt2addmuld  12464  div4p1lem1div2  12469  mul2lt0rgt0  13079  prodge0ld  13084  xrmax1  13156  xrmax2  13157  max1ALT  13167  qbtwnxr  13181  xleadd1a  13234  xlt2add  13241  xlesubadd  13244  xmulgt0  13264  xlemul1a  13269  xov1plusxeqvd  13477  uzsubsubfz  13525  fzctr  13615  subfzo0  13756  flflp1  13774  fldiv4lem1div2uz2  13803  ceilge  13812  modge0  13846  modlt  13847  modid  13863  m1modge3gt1  13885  modaddmodup  13901  sermono  14002  seqf1olem1  14009  seqf1olem2  14010  sqgt0  14093  sqge0  14103  leexp1a  14142  nnlesq  14171  expnbnd  14197  expmulnbnd  14200  discr1  14204  facwordi  14251  faclbnd5  14260  nfile  14321  hashdom  14341  hashgt23el  14386  fi1uzind  14460  brfi1indALT  14463  ccatws1n0  14584  swrds2  14893  cjmulge0  15095  resqrtcl  15202  absge0  15236  sqreulem  15308  amgm2  15318  rlimdm  15497  rlimge0  15527  reccn2  15543  climle  15586  climserle  15611  isercoll2  15617  iseraltlem1  15630  iseralt  15633  isumclim2  15706  isumclim3  15707  isumge0  15714  fsumless  15744  cvgcmp  15764  cvgcmpce  15766  abscvgcvg  15767  isumsup2  15794  isumltss  15796  climcndslem1  15797  climcnds  15799  supcvg  15804  harmonic  15807  expcnv  15812  explecnv  15813  cvgrat  15831  mertenslem1  15832  mertenslem2  15833  clim2div  15837  ntrivcvgtail  15848  iprodclim2  15945  iprodclim3  15946  efcvg  16030  ege2le3  16035  efaddlem  16038  eftlub  16054  effsumlt  16056  tanhlt1  16105  ef01bndlem  16129  sin02gt0  16137  rpnnen2lem4  16162  ruclem2  16177  ruclem3  16178  ruclem9  16183  iddvdsexp  16225  dvdsadd  16247  dvdsfac  16271  dvdsexp2im  16272  dvdsmod  16274  3dvds  16276  omoe  16309  sumeven  16332  divalglem1  16339  flodddiv4t2lthalf  16361  bitsfzo  16378  bitsmod  16379  bitscmp  16381  bitsinv1lem  16384  sadcaddlem  16400  sadadd3  16404  sadaddlem  16409  dvdssqim  16498  dvdsmulgcd  16499  nn0seqcvgd  16509  dvdslcm  16537  lcmgcdlem  16545  dvdslcmf  16570  lcmfunsnlem2lem2  16578  mulgcddvds  16594  qredeq  16596  cncongr2  16607  sqnprm  16641  isprm6  16653  nonsq  16697  hashdvds  16710  prmdiv  16720  odzdvds  16730  pythagtriplem4  16754  pcpre1  16777  pcdvdsb  16804  pcz  16816  pcprmpw2  16817  pcaddlem  16823  pcadd  16824  pcadd2  16825  pcmpt  16827  pcmptdvds  16829  fldivp1  16832  pcfaclem  16833  pockthlem  16840  prmreclem1  16851  prmreclem3  16853  prmreclem5  16855  prmreclem6  16856  4sqlem6  16878  4sqlem8  16880  4sqlem11  16890  4sqlem12  16891  4sqlem14  16893  4sqlem16  16895  vdwlem3  16918  vdwlem9  16924  vdwlem10  16925  vdwlem12  16927  ramub1lem2  16962  prmgap  16994  prmgaplcm  16995  prmgapprmo  16997  mreexexd  17594  invfuc  17929  ple1  18385  eqgen  19063  lagsubg  19074  pgpfi  19475  sylow2alem2  19488  sylow2a  19489  sylow3lem4  19500  efgsrel  19604  odadd1  19718  odadd2  19719  gexex  19723  lt6abl  19765  dprd2d2  19916  dmdprdpr  19921  ablfacrp2  19939  ablfac1c  19943  pgpfaclem1  19953  ablfac2  19961  fincygsubgodd  19984  dvdsrmul1  20187  unitmulclb  20199  subrguss  20338  abvres  20451  znfld  21122  znunit  21125  frlmisfrlm  21409  ply1coefsupp  21826  evl1gsumadd  21884  matgsum  21946  pm2mpcl  22306  psmetxrge0  23826  isxmet2d  23840  mettri  23865  xmettri3  23866  mettri3  23867  xmetrtri2  23869  prdsxmetlem  23881  imasdsf1olem  23886  xblss2ps  23914  blss2ps  23916  blss2  23917  blssps  23937  blss  23938  prdsbl  24007  dscmet  24088  nmge0  24133  nmmtri  24138  tngngp3  24180  nlmvscnlem2  24209  nrginvrcnlem  24215  nmoix  24253  nmoleub  24255  blcvx  24321  xrsxmet  24332  opnreen  24354  xrge0tsms  24357  icopnfcnv  24465  xrhmeo  24469  lebnumii  24489  pcophtb  24552  pi1grplem  24572  nmoleub2lem  24637  ipcau2  24758  tcphcphlem1  24759  ipcau  24762  ipcnlem2  24768  rrxcph  24916  minveclem2  24950  minveclem3b  24952  pjthlem1  24961  pjthlem2  24962  ivthlem3  24977  ivth2  24979  ovolfsf  24995  ovolsslem  25008  ovollb2lem  25012  ovollb2  25013  ovolctb  25014  ovolfiniun  25025  ovolicc1  25040  ovolicc2lem4  25044  ovolicc2  25046  nulmbl2  25060  unmbl  25061  ioombl1lem4  25085  uniioombllem4  25110  uniioombllem6  25112  volivth  25131  vitalilem4  25135  itg1ge0  25210  itg1ge0a  25236  itg1lea  25237  itg1climres  25239  mbfi1fseqlem5  25244  itg2ub  25258  itg2seq  25267  itg2uba  25268  itg2splitlem  25273  itg2split  25274  itg2monolem3  25277  itg2mono  25278  itg2i1fseq2  25281  itg2addlem  25283  iblss  25329  itggt0  25368  dvferm2lem  25510  dvlip  25517  dvivthlem1  25532  dvfsumlem2  25551  dvfsumlem3  25552  ftc1lem4  25563  ply1divmo  25660  ply1remlem  25687  fta1glem2  25691  ig1pdvds  25701  plyeq0lem  25731  plydiveu  25818  fta1lem  25827  vieta1lem2  25831  aaliou3lem2  25863  aaliou3lem8  25865  ulmcn  25918  mtest  25923  itgulm  25927  radcnvlem1  25932  radcnvlt1  25937  dvradcnv  25940  pserdvlem2  25947  abelthlem2  25951  abelthlem6  25955  abelthlem7  25957  abelthlem9  25959  tangtx  26022  sinq12gt0  26024  sineq0  26040  cosordlem  26046  tanord  26054  tanregt0  26055  logrnaddcl  26090  logcj  26121  argregt0  26125  argrege0  26126  argimgt0  26127  argimlt0  26128  logimul  26129  logneg2  26130  logdivlti  26135  divlogrlim  26150  logcnlem3  26159  logcnlem4  26160  dvlog2lem  26167  logtayl  26175  rpcxpcl  26191  cxpsqrtlem  26217  cxpaddle  26267  isosctrlem1  26330  asinlem3a  26382  asinlem3  26383  asinneg  26398  asinsinlem  26403  asinsin  26404  atanlogaddlem  26425  atanlogadd  26426  atanlogsublem  26427  atanlogsub  26428  atantan  26435  atanbndlem  26437  atantayl  26449  leibpi  26454  birthdaylem3  26465  areaf  26473  cxploglim  26489  jensenlem2  26499  jensen  26500  logdiflbnd  26506  harmonicbnd4  26522  fsumharmonic  26523  zetacvg  26526  lgamgulmlem2  26541  lgamgulmlem3  26542  lgamcvg2  26566  wilthlem2  26580  wilthimp  26583  ftalem1  26584  ftalem2  26585  ftalem5  26588  basellem6  26597  basellem8  26599  basellem9  26600  chtge0  26623  chtublem  26721  logexprlim  26735  perfectlem1  26739  bcmax  26788  bposlem1  26794  bposlem2  26795  bposlem6  26799  bposlem7  26800  lgsdilem2  26843  lgsqrlem4  26859  lgsquadlem1  26890  2lgsoddprmlem2  26919  2sqlem3  26930  2sqlem8  26936  2sqblem  26941  2sqmod  26946  chebbnd1lem2  26980  chtppilimlem1  26983  chtppilim  26985  chto1ub  26986  vmadivsum  26992  rplogsumlem1  26994  rplogsumlem2  26995  dchrisum0lem1a  26996  rpvmasumlem  26997  dchrisumlem1  26999  dchrisumlem2  27000  dchrvmasumlem2  27008  dchrisum0flblem1  27018  dchrisum0flblem2  27019  dchrisum0lem1b  27025  dchrisum0lem1  27026  dchrisum0lem2a  27027  dchrisum0lem3  27029  dchrisum0  27030  mudivsum  27040  mulogsumlem  27041  mulog2sumlem1  27044  mulog2sumlem2  27045  2vmadivsumlem  27050  chpdifbndlem1  27063  selberg3lem1  27067  selberg4lem1  27070  pntrlog2bndlem1  27087  pntrlog2bndlem2  27088  pntrlog2bndlem3  27089  pntrlog2bndlem4  27090  pntpbnd1a  27095  pntpbnd1  27096  pntpbnd2  27097  pntibndlem2  27101  pntibndlem3  27102  pntlemd  27104  pntlemc  27105  pntlemb  27107  pntlemg  27108  pntlemh  27109  pntlemr  27112  pntlemf  27115  pntlemo  27117  abvcxp  27125  ostth2lem1  27128  padicabv  27140  ostth2lem2  27144  ostth2lem3  27145  ostth2lem4  27146  ostth2  27147  ostth3  27148  nodense  27202  nogt01o  27206  nosupbnd2lem1  27225  noetasuplem3  27245  maxs1  27275  maxs2  27276  cofcutr  27420  cofcutrtime  27423  addsuniflem  27494  negsunif  27539  ssltmul2  27613  precsexlem11  27673  tgcgr4  27820  legso  27888  krippenlem  27979  midex  28026  oppperpex  28042  ttgcontlem1  28180  axpaschlem  28236  axcontlem8  28267  upgrex  28390  nbfusgrlevtxm1  28672  finsumvtxdgeven  28847  wwlksnextproplem3  29203  clwlkclwwlk2  29294  clwlkclwwlkfolem  29298  clwwlkndivn  29371  ex-ind-dvds  29752  nvabs  29963  nmooge0  30058  nmoolb  30062  siii  30144  minvecolem2  30166  minvecolem4  30171  minvecolem5  30172  hlipgt0  30205  normge0  30417  normpyc  30437  pjhthlem1  30682  pjige0i  30981  nmoplb  31198  nmfnlb  31215  branmfn  31396  pjssdif2i  31465  stlei  31531  xlt2addrd  32009  eliccelico  32026  elicoelioo  32027  bcm1n  32044  dvdszzq  32059  prmdvdsbc  32060  fsumiunle  32073  pfxlsw2ccat  32154  wrdt2ind  32155  xrge0tsmsd  32250  omndmul2  32271  psgnfzto1stlem  32300  cycpmco2lem4  32329  cycpmco2lem5  32330  cyc3conja  32357  archirngz  32376  archiabllem2c  32382  ofldchr  32473  fedgmullem2  32774  extdggt0  32795  evls1fldgencl  32804  algextdeglem8  32840  madjusmdetlem2  32877  locfinreflem  32889  xrge0iifiso  32984  nexple  33076  gsumesum  33126  esumcst  33130  esumpcvgval  33145  esumcvg  33153  esumiun  33161  measssd  33282  measunl  33283  omssubadd  33368  carsgclctunlem3  33388  pmeasmono  33392  sibfof  33408  oddpwdc  33422  eulerpartlemgc  33430  iwrdsplit  33455  ballotlemsgt1  33578  ballotlemsel1i  33580  sgnmul  33610  signsply0  33631  signstfvc  33654  signsvtp  33663  signsvfpn  33665  fdvposlt  33680  fdvneggt  33681  fdvnegge  33683  logdivsqrle  33731  hgt750lemf  33734  tgoldbachgtde  33741  swrdwlk  34186  subfaclim  34248  erdszelem7  34257  erdszelem8  34258  cvmliftlem2  34346  snmlff  34389  sinccvglem  34726  climlec3  34772  faclim  34785  gg-dvfsumlem2  35252  fnejoin1  35339  poimirlem12  36586  poimirlem17  36591  poimirlem19  36593  poimirlem20  36594  poimirlem23  36597  poimirlem28  36602  broucube  36608  mblfinlem2  36612  mblfinlem3  36613  mblfinlem4  36614  ismblfin  36615  itg2addnclem  36625  itg2addnclem3  36627  itg2gt0cn  36629  itggt0cn  36644  ftc1anclem5  36651  ftc1anclem7  36653  ftc1anclem8  36654  isbnd3  36738  ssbnd  36742  heiborlem8  36772  bfplem2  36777  rrncmslem  36786  rrnequiv  36789  rrntotbnd  36790  lcv1  37997  lsatcv0eq  38003  lsatcvat3  38008  cvlsupr2  38299  hlatlej2  38332  cvrval4N  38371  cvratlem  38378  atcvr0eq  38383  2atlt  38396  atbtwnex  38405  athgt  38413  1cvrat  38433  ps-1  38434  hlatexch3N  38437  hlatexch4  38438  3atlem2  38441  atcvrlln2  38476  lplnexllnN  38521  4atlem3a  38554  4atlem10b  38562  4atlem11b  38565  4atlem12b  38568  2lplnja  38576  dalemply  38611  dalemsly  38612  dalem1  38616  dalem6  38625  dalem7  38626  dalem-cly  38628  dalem11  38631  dalem12  38632  dalem16  38636  dalem17  38637  dalem38  38667  dalem44  38673  dalem61  38690  lnatexN  38736  lncvrat  38739  lncmp  38740  paddasslem2  38778  dalawlem3  38830  dalawlem6  38833  dalawlem11  38838  lhpmcvr  38980  lhp2atne  38991  lhp2at0ne  38993  lautj  39050  trlval4  39145  cdlemc2  39149  cdlemc5  39152  cdleme3b  39186  cdleme11c  39218  cdleme19a  39260  cdleme20j  39275  cdleme22f  39303  cdleme23c  39308  cdleme26f2ALTN  39321  cdleme26f2  39322  cdleme35fnpq  39406  cdleme48bw  39459  cdlemg10a  39597  cdlemg11b  39599  cdlemg17g  39624  cdlemg18c  39637  cdlemi1  39775  cdlemk52  39911  dia2dimlem1  40021  dihord1  40175  dihjatcclem4  40378  lcmineqlem15  40994  lcmineqlem19  40998  lcmineqlem22  41001  aks4d1lem1  41013  aks4d1p1p4  41022  aks4d1p1p5  41026  aks4d1p2  41028  aks4d1p3  41029  aks4d1p6  41032  aks4d1p7d1  41033  aks4d1p7  41034  aks4d1p8  41038  aks4d1p9  41039  sticksstones7  41054  metakunt7  41077  metakunt15  41085  metakunt16  41086  2xp3dxp2ge1d  41108  dvdsexpim  41301  dvdsexpnn0  41314  prjspner01  41449  flt4lem5  41474  fltnltalem  41486  fltnlta  41487  3cubeslem1  41504  eldioph2lem1  41580  lzenom  41590  irrapxlem1  41642  irrapxlem4  41645  irrapxlem5  41646  pell14qrgt0  41679  pell1qrge1  41690  pell1qrgap  41694  pellfundge  41702  pellfundex  41706  pellfund14  41718  rmspecsqrtnq  41726  rmxypos  41768  ltrmynn0  41769  ltrmxnn0  41770  jm2.24nn  41780  jm2.17b  41782  jm2.17c  41783  jm2.24  41784  congadd  41787  congsym  41789  congneg  41790  congid  41792  mzpcong  41793  acongrep  41801  acongeq  41804  jm2.18  41809  jm2.19  41814  jm2.23  41817  jm2.25  41820  jm2.26lem3  41822  jm2.15nn0  41824  jm2.16nn0  41825  jm2.27a  41826  jm2.27c  41828  jm3.1lem1  41838  idomrootle  42019  idomsubgmo  42022  sqrtcval  42474  inductionexd  42988  imo72b2  43006  dvgrat  43153  radcnvrat  43155  binomcxplemnn0  43190  binomcxplemnotnn0  43197  cncmpmax  43798  rnmptlb  44026  zltlesub  44074  infxrpnf  44235  xrpnf  44275  fmul01  44375  fmul01lt1lem1  44379  climdivf  44407  sumnnodd  44425  climinf2lem  44501  limsup10exlem  44567  climliminf  44601  dfxlim2v  44642  xlimliminflimsup  44657  dvdivbd  44718  volge0  44756  stoweidlem1  44796  stoweidlem16  44811  stoweidlem18  44813  stoweidlem24  44819  stoweidlem26  44821  stoweidlem36  44831  stoweidlem38  44833  stoweidlem41  44836  stoweidlem42  44837  stoweidlem44  44839  stoweidlem45  44840  stoweidlem48  44843  stoweidlem62  44857  wallispilem5  44864  stirlinglem1  44869  stirlinglem5  44873  stirlinglem7  44875  stirlinglem8  44876  stirlinglem9  44877  stirlinglem11  44879  fourierdlem4  44906  fourierdlem10  44912  fourierdlem37  44939  fourierdlem47  44948  fourierdlem72  44973  fourierdlem74  44975  fourierdlem79  44980  fourierdlem82  44983  fourierdlem89  44990  fourierdlem91  44992  fourierdlem93  44994  fourierdlem103  45004  fourierdlem104  45005  fourierdlem112  45013  etransclem24  45053  etransclem25  45054  etransclem28  45057  etransclem37  45066  etransclem38  45067  etransclem44  45073  meaiuninc3v  45279  vonicclem1  45478  pimconstlt0  45496  smfsuplem1  45606  rlimdmafv  45964  rlimdmafv2  46045  2elfz2melfz  46105  iccpartgtprec  46167  iccpartlt  46171  iccpartgtl  46173  sqrtpwpw2p  46285  fmtnodvds  46291  goldbachthlem1  46292  lighneallem4a  46355  perfectALTVlem1  46468  cznnring  46933  rhmsubcrngc  47006  altgsumbcALT  47108  expnegico01  47277  flnn0div2ge  47297  rege1logbrege0  47322  fllogbd  47324  nnpw2blen  47344  nnolog2flm1  47354  dignn0ldlem  47366  dignn0flhalflem1  47379  dignn0flhalflem2  47380  eenglngeehlnmlem2  47502  itsclc0yqsol  47528  2itscp  47545  itscnhlinecirc02plem1  47546  itscnhlinecirc02plem2  47547  inlinecirc02p  47551