MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqtrrd Structured version   Visualization version   GIF version

Theorem breqtrrd 4879
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
StepHypRef Expression
1 breqtrrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2819 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrd 4877 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   class class class wbr 4851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-br 4852
This theorem is referenced by:  marypha1lem  8581  marypha2  8587  unxpwdom  8736  uncdadom  9281  cdacomen  9291  cdaassen  9292  xpcdaen  9293  onacda  9307  infcdaabs  9316  cfss  9375  tskuni  9893  ltexnq  10085  lt2addmuld  11552  div4p1lem1div2  11557  mul2lt0rgt0  12150  prodge0ld  12155  xrmax1  12227  xrmax2  12228  max1ALT  12238  qbtwnxr  12252  xleadd1a  12304  xlt2add  12311  xlesubadd  12314  xmulgt0  12334  xlemul1a  12339  xov1plusxeqvd  12544  uzsubsubfz  12589  fzctr  12678  subfzo0  12817  flflp1  12835  fldiv4lem1div2uz2  12864  ceilge  12872  modge0  12905  modlt  12906  modid  12922  m1modge3gt1  12944  modaddmodup  12960  sermono  13059  seqf1olem1  13066  seqf1olem2  13067  leexp1a  13145  sqgt0  13158  sqge0  13166  nnlesq  13194  expnbnd  13219  expmulnbnd  13222  discr1  13226  facwordi  13299  faclbnd5  13308  nfile  13371  hashdom  13389  fi1uzind  13499  brfi1indALT  13502  ccatws1n0  13634  ccatws1n0OLD  13635  swrds2  13912  cjmulge0  14112  resqrtcl  14220  absge0  14253  sqreulem  14325  amgm2  14335  rlimdm  14508  rlimge0  14538  reccn2  14553  climle  14596  climserle  14619  isercoll2  14625  iseraltlem1  14638  iseralt  14641  isumclim2  14715  isumclim3  14716  isumge0  14723  fsumless  14753  cvgcmp  14773  cvgcmpce  14775  abscvgcvg  14776  isumsup2  14803  isumltss  14805  climcndslem1  14806  climcnds  14808  supcvg  14813  harmonic  14816  expcnv  14821  explecnv  14822  cvgrat  14839  mertenslem1  14840  mertenslem2  14841  clim2div  14845  ntrivcvgtail  14856  iprodclim2  14953  iprodclim3  14954  efcvg  15038  ege2le3  15043  efaddlem  15046  eftlub  15062  effsumlt  15064  tanhlt1  15113  ef01bndlem  15137  sin02gt0  15145  rpnnen2lem4  15169  ruclem2  15184  ruclem3  15185  ruclem9  15190  iddvdsexp  15231  dvdsadd  15250  dvdsfac  15274  dvdsmod  15276  3dvds  15278  omoe  15311  sumeven  15333  divalglem1  15340  flodddiv4t2lthalf  15362  bitsfzo  15379  bitsmod  15380  bitscmp  15382  bitsinv1lem  15385  sadcaddlem  15401  sadadd3  15405  sadaddlem  15410  dvdssqim  15495  dvdsmulgcd  15496  nn0seqcvgd  15505  dvdslcm  15533  lcmgcdlem  15541  dvdslcmf  15566  lcmfunsnlem2lem2  15574  mulgcddvds  15590  qredeq  15592  cncongr2  15603  sqnprm  15634  isprm6  15646  nonsq  15687  hashdvds  15700  prmdiv  15710  odzdvds  15720  pythagtriplem4  15744  pcpre1  15767  pcdvdsb  15793  pcz  15805  pcprmpw2  15806  pcaddlem  15812  pcadd  15813  pcadd2  15814  pcmpt  15816  pcmptdvds  15818  fldivp1  15821  pcfaclem  15822  pockthlem  15829  prmreclem1  15840  prmreclem3  15842  prmreclem5  15844  prmreclem6  15845  4sqlem6  15867  4sqlem8  15869  4sqlem11  15879  4sqlem12  15880  4sqlem14  15882  4sqlem16  15884  vdwlem3  15907  vdwlem9  15913  vdwlem10  15914  vdwlem12  15916  ramub1lem2  15951  prmgap  15983  prmgaplcm  15984  prmgapprmo  15986  mreexexd  16516  invfuc  16841  ple1  17252  eqgen  17852  lagsubg  17861  pgpfi  18224  sylow2alem2  18237  sylow2a  18238  sylow3lem4  18249  efgsrel  18351  odadd1  18455  odadd2  18456  gexex  18460  lt6abl  18500  dprd2d2  18648  dmdprdpr  18653  ablfacrp2  18671  ablfac1c  18675  pgpfaclem1  18685  ablfac2  18693  dvdsrmul1  18858  unitmulclb  18870  subrguss  19002  abvres  19046  ply1coefsupp  19876  evl1gsumadd  19933  znfld  20119  znunit  20122  frlmisfrlm  20401  matgsum  20457  pm2mpcl  20819  psmetxrge0  22335  isxmet2d  22349  mettri  22374  xmettri3  22375  mettri3  22376  xmetrtri2  22378  prdsxmetlem  22390  imasdsf1olem  22395  xblss2ps  22423  blss2ps  22425  blss2  22426  blssps  22446  blss  22447  prdsbl  22513  dscmet  22594  nmge0  22638  nmmtri  22643  tngngp3  22677  nlmvscnlem2  22706  nrginvrcnlem  22712  nmoix  22750  nmoleub  22752  blcvx  22818  xrsxmet  22829  opnreen  22851  xrge0tsms  22854  icopnfcnv  22958  xrhmeo  22962  lebnumii  22982  pcophtb  23045  pi1grplem  23065  nmoleub2lem  23130  ipcau2  23249  tchcphlem1  23250  ipcau  23253  ipcnlem2  23259  rrxcph  23398  minveclem2  23415  minveclem3b  23417  pjthlem1  23426  pjthlem2  23427  ivthlem3  23440  ivth2  23442  ovolfsf  23458  ovolsslem  23471  ovollb2lem  23475  ovollb2  23476  ovolctb  23477  ovolfiniun  23488  ovolicc1  23503  ovolicc2lem4  23507  ovolicc2  23509  nulmbl2  23523  unmbl  23524  ioombl1lem4  23548  uniioombllem4  23573  uniioombllem6  23575  volivth  23594  vitalilem4  23598  itg1ge0  23673  itg1ge0a  23698  itg1lea  23699  itg1climres  23701  mbfi1fseqlem5  23706  itg2ub  23720  itg2seq  23729  itg2uba  23730  itg2splitlem  23735  itg2split  23736  itg2monolem3  23739  itg2mono  23740  itg2i1fseq2  23743  itg2addlem  23745  iblss  23791  itggt0  23828  dvferm2lem  23969  dvlip  23976  dvivthlem1  23991  dvfsumlem2  24010  dvfsumlem3  24011  ftc1lem4  24022  ply1divmo  24115  ply1remlem  24142  fta1glem2  24146  ig1pdvds  24156  plyeq0lem  24186  plydiveu  24273  fta1lem  24282  vieta1lem2  24286  aaliou3lem2  24318  aaliou3lem8  24320  ulmcn  24373  mtest  24378  itgulm  24382  radcnvlem1  24387  radcnvlt1  24392  dvradcnv  24395  pserdvlem2  24402  abelthlem2  24406  abelthlem6  24410  abelthlem7  24412  abelthlem9  24414  tangtx  24478  sinq12gt0  24480  sineq0  24494  cosordlem  24498  tanord  24505  tanregt0  24506  logrnaddcl  24541  logcj  24572  argregt0  24576  argrege0  24577  argimgt0  24578  argimlt0  24579  logimul  24580  logneg2  24581  logdivlti  24586  divlogrlim  24601  logcnlem3  24610  logcnlem4  24611  dvlog2lem  24618  logtayl  24626  rpcxpcl  24642  cxpsqrtlem  24668  cxpaddle  24713  isosctrlem1  24768  asinlem3a  24817  asinlem3  24818  asinneg  24833  asinsinlem  24838  asinsin  24839  atanlogaddlem  24860  atanlogadd  24861  atanlogsublem  24862  atanlogsub  24863  atantan  24870  atanbndlem  24872  atantayl  24884  leibpi  24889  birthdaylem3  24900  areaf  24908  cxploglim  24924  jensenlem2  24934  jensen  24935  logdiflbnd  24941  harmonicbnd4  24957  fsumharmonic  24958  zetacvg  24961  lgamgulmlem2  24976  lgamgulmlem3  24977  lgamcvg2  25001  wilthlem2  25015  wilthimp  25018  ftalem1  25019  ftalem2  25020  ftalem5  25023  basellem6  25032  basellem8  25034  basellem9  25035  chtge0  25058  chtublem  25156  logexprlim  25170  perfectlem1  25174  bcmax  25223  bposlem1  25229  bposlem2  25230  bposlem6  25234  bposlem7  25235  lgsdilem2  25278  lgsqrlem4  25294  lgsquadlem1  25325  2lgsoddprmlem2  25354  2sqlem3  25365  2sqlem8  25371  2sqblem  25376  chebbnd1lem2  25379  chtppilimlem1  25382  chtppilim  25384  chto1ub  25385  vmadivsum  25391  rplogsumlem1  25393  rplogsumlem2  25394  dchrisum0lem1a  25395  rpvmasumlem  25396  dchrisumlem1  25398  dchrisumlem2  25399  dchrvmasumlem2  25407  dchrisum0flblem1  25417  dchrisum0flblem2  25418  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0lem3  25428  dchrisum0  25429  mudivsum  25439  mulogsumlem  25440  mulog2sumlem1  25443  mulog2sumlem2  25444  2vmadivsumlem  25449  chpdifbndlem1  25462  selberg3lem1  25466  selberg4lem1  25469  pntrlog2bndlem1  25486  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem4  25489  pntpbnd1a  25494  pntpbnd1  25495  pntpbnd2  25496  pntibndlem2  25500  pntibndlem3  25501  pntlemd  25503  pntlemc  25504  pntlemb  25506  pntlemg  25507  pntlemh  25508  pntlemr  25511  pntlemf  25514  pntlemo  25516  abvcxp  25524  ostth2lem1  25527  padicabv  25539  ostth2lem2  25543  ostth2lem3  25544  ostth2lem4  25545  ostth2  25546  ostth3  25547  tgcgr4  25646  legso  25714  krippenlem  25805  midex  25849  oppperpex  25865  ttgcontlem1  25985  axpaschlem  26040  axcontlem8  26071  upgrex  26207  nbfusgrlevtxm1  26501  finsumvtxdgeven  26682  wwlksnextproplem3  27055  clwlkclwwlk2  27152  clwlkclwwlkfolem  27156  clwwlkndivn  27237  clwlksf1clwwlklem1OLD  27245  ex-ind-dvds  27655  nvabs  27861  nmooge0  27956  nmoolb  27960  siii  28042  minvecolem2  28065  minvecolem4  28070  minvecolem5  28071  hlipgt0  28104  normge0  28317  normpyc  28337  pjhthlem1  28584  pjige0i  28883  nmoplb  29100  nmfnlb  29117  branmfn  29298  pjssdif2i  29367  stlei  29433  xlt2addrd  29856  eliccelico  29872  elicoelioo  29873  bcm1n  29887  fsumiunle  29908  2sqmod  29979  omndmul2  30043  archirngz  30074  archiabllem2c  30080  xrge0tsmsd  30116  ofldchr  30145  psgnfzto1stlem  30181  madjusmdetlem2  30225  locfinreflem  30238  xrge0iifiso  30312  nexple  30402  gsumesum  30452  esumcst  30456  esumpcvgval  30471  esumcvg  30479  esumiun  30487  measssd  30609  measunl  30610  omssubadd  30693  carsgclctunlem3  30713  pmeasmono  30717  sibfof  30733  oddpwdc  30747  eulerpartlemgc  30755  iwrdsplit  30780  ballotlemsgt1  30903  ballotlemsel1i  30905  sgnmul  30935  signsply0  30959  signstfvc  30982  signsvtp  30991  signsvfpn  30993  fdvposlt  31008  fdvneggt  31009  fdvnegge  31011  logdivsqrle  31059  hgt750lemf  31062  tgoldbachgtde  31069  subfaclim  31498  erdszelem7  31507  erdszelem8  31508  cvmliftlem2  31596  snmlff  31639  sinccvglem  31893  climlec3  31946  faclim  31959  dvdspw  31963  nodense  32168  nosupbnd2lem1  32187  noetalem2  32190  fnejoin1  32689  poimirlem12  33736  poimirlem17  33741  poimirlem19  33743  poimirlem20  33744  poimirlem23  33747  poimirlem28  33752  broucube  33758  mblfinlem2  33762  mblfinlem3  33763  mblfinlem4  33764  ismblfin  33765  itg2addnclem  33775  itg2addnclem3  33777  itg2gt0cn  33779  itggt0cn  33796  ftc1anclem5  33803  ftc1anclem7  33805  ftc1anclem8  33806  isbnd3  33896  ssbnd  33900  heiborlem8  33930  bfplem2  33935  rrncmslem  33944  rrnequiv  33947  rrntotbnd  33948  lcv1  34823  lsatcv0eq  34829  lsatcvat3  34834  cvlsupr2  35125  hlatlej2  35158  cvrval4N  35196  cvratlem  35203  atcvr0eq  35208  2atlt  35221  atbtwnex  35230  athgt  35238  1cvrat  35258  ps-1  35259  hlatexch3N  35262  hlatexch4  35263  3atlem2  35266  atcvrlln2  35301  lplnexllnN  35346  4atlem3a  35379  4atlem10b  35387  4atlem11b  35390  4atlem12b  35393  2lplnja  35401  dalemply  35436  dalemsly  35437  dalem1  35441  dalem6  35450  dalem7  35451  dalem-cly  35453  dalem11  35456  dalem12  35457  dalem16  35461  dalem17  35462  dalem38  35492  dalem44  35498  dalem61  35515  lnatexN  35561  lncvrat  35564  lncmp  35565  paddasslem2  35603  dalawlem3  35655  dalawlem6  35658  dalawlem11  35663  lhpmcvr  35805  lhp2atne  35816  lhp2at0ne  35818  lautj  35875  trlval4  35970  cdlemc2  35974  cdlemc5  35977  cdleme3b  36011  cdleme11c  36043  cdleme19a  36085  cdleme20j  36100  cdleme22f  36128  cdleme23c  36133  cdleme26f2ALTN  36146  cdleme26f2  36147  cdleme35fnpq  36231  cdleme48bw  36284  cdlemg10a  36422  cdlemg11b  36424  cdlemg17g  36449  cdlemg18c  36462  cdlemi1  36600  cdlemk52  36736  dia2dimlem1  36846  dihord1  37000  dihjatcclem4  37203  eldioph2lem1  37826  lzenom  37836  irrapxlem1  37889  irrapxlem4  37892  irrapxlem5  37893  pell14qrgt0  37926  pell1qrge1  37937  pell1qrgap  37941  pellfundge  37949  pellfundex  37953  pellfund14  37965  rmspecsqrtnq  37973  rmxypos  38016  ltrmynn0  38017  ltrmxnn0  38018  jm2.24nn  38028  jm2.17b  38030  jm2.17c  38031  jm2.24  38032  congadd  38035  congsym  38037  congneg  38038  congid  38040  mzpcong  38041  acongrep  38049  acongeq  38052  jm2.18  38057  jm2.19  38062  jm2.23  38065  jm2.25  38068  jm2.26lem3  38070  jm2.15nn0  38072  jm2.16nn0  38073  jm2.27a  38074  jm2.27c  38076  jm3.1lem1  38086  idomrootle  38275  idomsubgmo  38278  inductionexd  38954  imo72b2  38976  dvgrat  39012  radcnvrat  39014  binomcxplemnn0  39049  binomcxplemnotnn0  39056  cncmpmax  39686  rnmptlb  39938  zltlesub  39980  infxrpnf  40154  xrpnf  40196  fmul01  40293  fmul01lt1lem1  40297  climdivf  40325  sumnnodd  40343  climinf2lem  40419  limsup10exlem  40485  climliminf  40519  dfxlim2v  40554  dvdivbd  40619  volge0  40657  stoweidlem1  40698  stoweidlem16  40713  stoweidlem18  40715  stoweidlem24  40721  stoweidlem26  40723  stoweidlem36  40733  stoweidlem38  40735  stoweidlem41  40738  stoweidlem42  40739  stoweidlem44  40741  stoweidlem45  40742  stoweidlem48  40745  stoweidlem62  40759  wallispilem5  40766  stirlinglem1  40771  stirlinglem5  40775  stirlinglem7  40777  stirlinglem8  40778  stirlinglem9  40779  stirlinglem11  40781  fourierdlem4  40808  fourierdlem10  40814  fourierdlem37  40841  fourierdlem47  40850  fourierdlem72  40875  fourierdlem74  40877  fourierdlem79  40882  fourierdlem82  40885  fourierdlem89  40892  fourierdlem91  40894  fourierdlem93  40896  fourierdlem103  40906  fourierdlem104  40907  fourierdlem112  40915  etransclem24  40955  etransclem25  40956  etransclem28  40959  etransclem37  40968  etransclem38  40969  etransclem44  40975  meaiuninc3v  41181  vonicclem1  41380  pimconstlt0  41397  smfsuplem1  41500  rlimdmafv  41767  rlimdmafv2  41848  2elfz2melfz  41904  iccpartgtprec  41932  iccpartlt  41936  iccpartgtl  41938  sqrtpwpw2p  42026  fmtnodvds  42032  goldbachthlem1  42033  lighneallem4a  42101  perfectALTVlem1  42206  cznnring  42525  rhmsubcrngc  42598  altgsumbcALT  42700  expnegico01  42877  flnn0div2ge  42896  rege1logbrege0  42921  fllogbd  42923  fllog2  42931  nnpw2blen  42943  nnolog2flm1  42953  dignn0ldlem  42965  dignn0flhalflem1  42978  dignn0flhalflem2  42979
  Copyright terms: Public domain W3C validator