Theorem breqtrrd 5094

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  marypha1lem  8897  marypha2  8903  infsupprpr  8968  unxpwdom  9053  onadju  9619  cfss  9687  tskuni  10205  ltexnq  10397  lt2addmuld  11888  div4p1lem1div2  11893  mul2lt0rgt0  12493  prodge0ld  12498  xrmax1  12569  xrmax2  12570  max1ALT  12580  qbtwnxr  12594  xleadd1a  12647  xlt2add  12654  xlesubadd  12657  xmulgt0  12677  xlemul1a  12682  xov1plusxeqvd  12885  uzsubsubfz  12930  fzctr  13020  subfzo0  13160  flflp1  13178  fldiv4lem1div2uz2  13207  ceilge  13215  modge0  13248  modlt  13249  modid  13265  m1modge3gt1  13287  modaddmodup  13303  sermono  13403  seqf1olem1  13410  seqf1olem2  13411  sqgt0  13492  sqge0  13502  leexp1a  13540  nnlesq  13569  expnbnd  13594  expmulnbnd  13597  discr1  13601  facwordi  13650  faclbnd5  13659  nfile  13721  hashdom  13741  hashgt23el  13786  fi1uzind  13856  brfi1indALT  13859  ccatws1n0  13991  swrds2  14302  cjmulge0  14505  resqrtcl  14613  absge0  14647  sqreulem  14719  amgm2  14729  rlimdm  14908  rlimge0  14938  reccn2  14953  climle  14996  climserle  15019  isercoll2  15025  iseraltlem1  15038  iseralt  15041  isumclim2  15113  isumclim3  15114  isumge0  15121  fsumless  15151  cvgcmp  15171  cvgcmpce  15173  abscvgcvg  15174  isumsup2  15201  isumltss  15203  climcndslem1  15204  climcnds  15206  supcvg  15211  harmonic  15214  expcnv  15219  explecnv  15220  cvgrat  15239  mertenslem1  15240  mertenslem2  15241  clim2div  15245  ntrivcvgtail  15256  iprodclim2  15353  iprodclim3  15354  efcvg  15438  ege2le3  15443  efaddlem  15446  eftlub  15462  effsumlt  15464  tanhlt1  15513  ef01bndlem  15537  sin02gt0  15545  rpnnen2lem4  15570  ruclem2  15585  ruclem3  15586  ruclem9  15591  iddvdsexp  15633  dvdsadd  15652  dvdsfac  15676  dvdsmod  15678  3dvds  15680  omoe  15713  sumeven  15738  divalglem1  15745  flodddiv4t2lthalf  15767  bitsfzo  15784  bitsmod  15785  bitscmp  15787  bitsinv1lem  15790  sadcaddlem  15806  sadadd3  15810  sadaddlem  15815  dvdssqim  15904  dvdsmulgcd  15905  nn0seqcvgd  15914  dvdslcm  15942  lcmgcdlem  15950  dvdslcmf  15975  lcmfunsnlem2lem2  15983  mulgcddvds  15999  qredeq  16001  cncongr2  16012  sqnprm  16046  isprm6  16058  nonsq  16099  hashdvds  16112  prmdiv  16122  odzdvds  16132  pythagtriplem4  16156  pcpre1  16179  pcdvdsb  16205  pcz  16217  pcprmpw2  16218  pcaddlem  16224  pcadd  16225  pcadd2  16226  pcmpt  16228  pcmptdvds  16230  fldivp1  16233  pcfaclem  16234  pockthlem  16241  prmreclem1  16252  prmreclem3  16254  prmreclem5  16256  prmreclem6  16257  4sqlem6  16279  4sqlem8  16281  4sqlem11  16291  4sqlem12  16292  4sqlem14  16294  4sqlem16  16296  vdwlem3  16319  vdwlem9  16325  vdwlem10  16326  vdwlem12  16328  ramub1lem2  16363  prmgap  16395  prmgaplcm  16396  prmgapprmo  16398  mreexexd  16919  invfuc  17244  ple1  17654  eqgen  18333  lagsubg  18342  pgpfi  18730  sylow2alem2  18743  sylow2a  18744  sylow3lem4  18755  efgsrel  18860  odadd1  18968  odadd2  18969  gexex  18973  lt6abl  19015  dprd2d2  19166  dmdprdpr  19171  ablfacrp2  19189  ablfac1c  19193  pgpfaclem1  19203  ablfac2  19211  fincygsubgodd  19234  dvdsrmul1  19403  unitmulclb  19415  subrguss  19550  abvres  19610  ply1coefsupp  20463  evl1gsumadd  20521  znfld  20707  znunit  20710  frlmisfrlm  20992  matgsum  21046  pm2mpcl  21405  psmetxrge0  22923  isxmet2d  22937  mettri  22962  xmettri3  22963  mettri3  22964  xmetrtri2  22966  prdsxmetlem  22978  imasdsf1olem  22983  xblss2ps  23011  blss2ps  23013  blss2  23014  blssps  23034  blss  23035  prdsbl  23101  dscmet  23182  nmge0  23226  nmmtri  23231  tngngp3  23265  nlmvscnlem2  23294  nrginvrcnlem  23300  nmoix  23338  nmoleub  23340  blcvx  23406  xrsxmet  23417  opnreen  23439  xrge0tsms  23442  icopnfcnv  23546  xrhmeo  23550  lebnumii  23570  pcophtb  23633  pi1grplem  23653  nmoleub2lem  23718  ipcau2  23837  tcphcphlem1  23838  ipcau  23841  ipcnlem2  23847  rrxcph  23995  minveclem2  24029  minveclem3b  24031  pjthlem1  24040  pjthlem2  24041  ivthlem3  24054  ivth2  24056  ovolfsf  24072  ovolsslem  24085  ovollb2lem  24089  ovollb2  24090  ovolctb  24091  ovolfiniun  24102  ovolicc1  24117  ovolicc2lem4  24121  ovolicc2  24123  nulmbl2  24137  unmbl  24138  ioombl1lem4  24162  uniioombllem4  24187  uniioombllem6  24189  volivth  24208  vitalilem4  24212  itg1ge0  24287  itg1ge0a  24312  itg1lea  24313  itg1climres  24315  mbfi1fseqlem5  24320  itg2ub  24334  itg2seq  24343  itg2uba  24344  itg2splitlem  24349  itg2split  24350  itg2monolem3  24353  itg2mono  24354  itg2i1fseq2  24357  itg2addlem  24359  iblss  24405  itggt0  24442  dvferm2lem  24583  dvlip  24590  dvivthlem1  24605  dvfsumlem2  24624  dvfsumlem3  24625  ftc1lem4  24636  ply1divmo  24729  ply1remlem  24756  fta1glem2  24760  ig1pdvds  24770  plyeq0lem  24800  plydiveu  24887  fta1lem  24896  vieta1lem2  24900  aaliou3lem2  24932  aaliou3lem8  24934  ulmcn  24987  mtest  24992  itgulm  24996  radcnvlem1  25001  radcnvlt1  25006  dvradcnv  25009  pserdvlem2  25016  abelthlem2  25020  abelthlem6  25024  abelthlem7  25026  abelthlem9  25028  tangtx  25091  sinq12gt0  25093  sineq0  25109  cosordlem  25115  tanord  25122  tanregt0  25123  logrnaddcl  25158  logcj  25189  argregt0  25193  argrege0  25194  argimgt0  25195  argimlt0  25196  logimul  25197  logneg2  25198  logdivlti  25203  divlogrlim  25218  logcnlem3  25227  logcnlem4  25228  dvlog2lem  25235  logtayl  25243  rpcxpcl  25259  cxpsqrtlem  25285  cxpaddle  25333  isosctrlem1  25396  asinlem3a  25448  asinlem3  25449  asinneg  25464  asinsinlem  25469  asinsin  25470  atanlogaddlem  25491  atanlogadd  25492  atanlogsublem  25493  atanlogsub  25494  atantan  25501  atanbndlem  25503  atantayl  25515  leibpi  25520  birthdaylem3  25531  areaf  25539  cxploglim  25555  jensenlem2  25565  jensen  25566  logdiflbnd  25572  harmonicbnd4  25588  fsumharmonic  25589  zetacvg  25592  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamcvg2  25632  wilthlem2  25646  wilthimp  25649  ftalem1  25650  ftalem2  25651  ftalem5  25654  basellem6  25663  basellem8  25665  basellem9  25666  chtge0  25689  chtublem  25787  logexprlim  25801  perfectlem1  25805  bcmax  25854  bposlem1  25860  bposlem2  25861  bposlem6  25865  bposlem7  25866  lgsdilem2  25909  lgsqrlem4  25925  lgsquadlem1  25956  2lgsoddprmlem2  25985  2sqlem3  25996  2sqlem8  26002  2sqblem  26007  2sqmod  26012  chebbnd1lem2  26046  chtppilimlem1  26049  chtppilim  26051  chto1ub  26052  vmadivsum  26058  rplogsumlem1  26060  rplogsumlem2  26061  dchrisum0lem1a  26062  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem2  26066  dchrvmasumlem2  26074  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem3  26095  dchrisum0  26096  mudivsum  26106  mulogsumlem  26107  mulog2sumlem1  26110  mulog2sumlem2  26111  2vmadivsumlem  26116  chpdifbndlem1  26129  selberg3lem1  26133  selberg4lem1  26136  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntibndlem3  26168  pntlemd  26170  pntlemc  26171  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemr  26178  pntlemf  26181  pntlemo  26183  abvcxp  26191  ostth2lem1  26194  padicabv  26206  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth2  26213  ostth3  26214  tgcgr4  26317  legso  26385  krippenlem  26476  midex  26523  oppperpex  26539  ttgcontlem1  26671  axpaschlem  26726  axcontlem8  26757  upgrex  26877  nbfusgrlevtxm1  27159  finsumvtxdgeven  27334  wwlksnextproplem3  27690  clwlkclwwlk2  27781  clwlkclwwlkfolem  27785  clwwlkndivn  27859  ex-ind-dvds  28240  nvabs  28449  nmooge0  28544  nmoolb  28548  siii  28630  minvecolem2  28652  minvecolem4  28657  minvecolem5  28658  hlipgt0  28691  normge0  28903  normpyc  28923  pjhthlem1  29168  pjige0i  29467  nmoplb  29684  nmfnlb  29701  branmfn  29882  pjssdif2i  29951  stlei  30017  xlt2addrd  30482  eliccelico  30500  elicoelioo  30501  bcm1n  30518  dvdszzq  30531  prmdvdsbc  30532  fsumiunle  30545  pfxlsw2ccat  30626  wrdt2ind  30627  xrge0tsmsd  30692  omndmul2  30713  psgnfzto1stlem  30742  cycpmco2lem4  30771  cycpmco2lem5  30772  cyc3conja  30799  archirngz  30818  archiabllem2c  30824  ofldchr  30887  fedgmullem2  31026  extdggt0  31047  madjusmdetlem2  31093  locfinreflem  31104  xrge0iifiso  31178  nexple  31268  gsumesum  31318  esumcst  31322  esumpcvgval  31337  esumcvg  31345  esumiun  31353  measssd  31474  measunl  31475  omssubadd  31558  carsgclctunlem3  31578  pmeasmono  31582  sibfof  31598  oddpwdc  31612  eulerpartlemgc  31620  iwrdsplit  31645  ballotlemsgt1  31768  ballotlemsel1i  31770  sgnmul  31800  signsply0  31821  signstfvc  31844  signsvtp  31853  signsvfpn  31855  fdvposlt  31870  fdvneggt  31871  fdvnegge  31873  logdivsqrle  31921  hgt750lemf  31924  tgoldbachgtde  31931  swrdwlk  32373  subfaclim  32435  erdszelem7  32444  erdszelem8  32445  cvmliftlem2  32533  snmlff  32576  sinccvglem  32915  climlec3  32965  faclim  32978  dvdspw  32982  nodense  33196  nosupbnd2lem1  33215  noetalem2  33218  fnejoin1  33716  poimirlem12  34919  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem23  34930  poimirlem28  34935  broucube  34941  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem  34958  itg2addnclem3  34960  itg2gt0cn  34962  itggt0cn  34979  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  isbnd3  35077  ssbnd  35081  heiborlem8  35111  bfplem2  35116  rrncmslem  35125  rrnequiv  35128  rrntotbnd  35129  lcv1  36192  lsatcv0eq  36198  lsatcvat3  36203  cvlsupr2  36494  hlatlej2  36527  cvrval4N  36565  cvratlem  36572  atcvr0eq  36577  2atlt  36590  atbtwnex  36599  athgt  36607  1cvrat  36627  ps-1  36628  hlatexch3N  36631  hlatexch4  36632  3atlem2  36635  atcvrlln2  36670  lplnexllnN  36715  4atlem3a  36748  4atlem10b  36756  4atlem11b  36759  4atlem12b  36762  2lplnja  36770  dalemply  36805  dalemsly  36806  dalem1  36810  dalem6  36819  dalem7  36820  dalem-cly  36822  dalem11  36825  dalem12  36826  dalem16  36830  dalem17  36831  dalem38  36861  dalem44  36867  dalem61  36884  lnatexN  36930  lncvrat  36933  lncmp  36934  paddasslem2  36972  dalawlem3  37024  dalawlem6  37027  dalawlem11  37032  lhpmcvr  37174  lhp2atne  37185  lhp2at0ne  37187  lautj  37244  trlval4  37339  cdlemc2  37343  cdlemc5  37346  cdleme3b  37380  cdleme11c  37412  cdleme19a  37454  cdleme20j  37469  cdleme22f  37497  cdleme23c  37502  cdleme26f2ALTN  37515  cdleme26f2  37516  cdleme35fnpq  37600  cdleme48bw  37653  cdlemg10a  37791  cdlemg11b  37793  cdlemg17g  37818  cdlemg18c  37831  cdlemi1  37969  cdlemk52  38105  dia2dimlem1  38215  dihord1  38369  dihjatcclem4  38572  2xp3dxp2ge1d  39117  cxpgt0d  39200  dvdsexpim  39201  fltnltalem  39294  fltnlta  39295  3cubeslem1  39301  eldioph2lem1  39377  lzenom  39387  irrapxlem1  39439  irrapxlem4  39442  irrapxlem5  39443  pell14qrgt0  39476  pell1qrge1  39487  pell1qrgap  39491  pellfundge  39499  pellfundex  39503  pellfund14  39515  rmspecsqrtnq  39523  rmxypos  39564  ltrmynn0  39565  ltrmxnn0  39566  jm2.24nn  39576  jm2.17b  39578  jm2.17c  39579  jm2.24  39580  congadd  39583  congsym  39585  congneg  39586  congid  39588  mzpcong  39589  acongrep  39597  acongeq  39600  jm2.18  39605  jm2.19  39610  jm2.23  39613  jm2.25  39616  jm2.26lem3  39618  jm2.15nn0  39620  jm2.16nn0  39621  jm2.27a  39622  jm2.27c  39624  jm3.1lem1  39634  idomrootle  39815  idomsubgmo  39818  inductionexd  40525  imo72b2  40545  dvgrat  40664  radcnvrat  40666  binomcxplemnn0  40701  binomcxplemnotnn0  40708  cncmpmax  41309  rnmptlb  41534  zltlesub  41571  infxrpnf  41741  xrpnf  41782  fmul01  41881  fmul01lt1lem1  41885  climdivf  41913  sumnnodd  41931  climinf2lem  42007  limsup10exlem  42073  climliminf  42107  dfxlim2v  42148  xlimliminflimsup  42163  dvdivbd  42228  volge0  42266  stoweidlem1  42306  stoweidlem16  42321  stoweidlem18  42323  stoweidlem24  42329  stoweidlem26  42331  stoweidlem36  42341  stoweidlem38  42343  stoweidlem41  42346  stoweidlem42  42347  stoweidlem44  42349  stoweidlem45  42350  stoweidlem48  42353  stoweidlem62  42367  wallispilem5  42374  stirlinglem1  42379  stirlinglem5  42383  stirlinglem7  42385  stirlinglem8  42386  stirlinglem9  42387  stirlinglem11  42389  fourierdlem4  42416  fourierdlem10  42422  fourierdlem37  42449  fourierdlem47  42458  fourierdlem72  42483  fourierdlem74  42485  fourierdlem79  42490  fourierdlem82  42493  fourierdlem89  42500  fourierdlem91  42502  fourierdlem93  42504  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  etransclem24  42563  etransclem25  42564  etransclem28  42567  etransclem37  42576  etransclem38  42577  etransclem44  42583  meaiuninc3v  42786  vonicclem1  42985  pimconstlt0  43002  smfsuplem1  43105  rlimdmafv  43396  rlimdmafv2  43477  2elfz2melfz  43538  iccpartgtprec  43600  iccpartlt  43604  iccpartgtl  43606  sqrtpwpw2p  43720  fmtnodvds  43726  goldbachthlem1  43727  lighneallem4a  43793  perfectALTVlem1  43906  cznnring  44247  rhmsubcrngc  44320  altgsumbcALT  44421  expnegico01  44593  flnn0div2ge  44613  rege1logbrege0  44638  fllogbd  44640  nnpw2blen  44660  nnolog2flm1  44670  dignn0ldlem  44682  dignn0flhalflem1  44695  dignn0flhalflem2  44696  eenglngeehlnmlem2  44745  itsclc0yqsol  44771  2itscp  44788  itscnhlinecirc02plem1  44789  itscnhlinecirc02plem2  44790  inlinecirc02p  44794