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

Theorem breqtrrd 4465
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1  |-  ( ph  ->  A R B )
breqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
breqtrrd  |-  ( ph  ->  A R C )

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2462 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4463 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440
This theorem is referenced by:  marypha1lem  7885  marypha2  7891  unxpwdom  8007  uncdadom  8542  cdacomen  8552  cdaassen  8553  xpcdaen  8554  onacda  8568  infcdaabs  8577  cfss  8636  tskuni  9150  ltexnq  9342  xrmax1  11379  xrmax2  11380  max1ALT  11390  qbtwnxr  11402  xleadd1a  11448  xlt2add  11455  xlesubadd  11458  xmulgt0  11478  xlemul1a  11483  xov1plusxeqvd  11669  uzsubsubfz  11710  fzctr  11791  flflp1  11925  ceilge  11955  modge0  11987  modlt  11988  modid  12002  modaddmodup  12032  sermono  12121  seqf1olem1  12128  seqf1olem2  12129  leexp1a  12206  sqgt0  12218  sqge0  12226  nnlesq  12253  expnbnd  12277  expmulnbnd  12280  discr1  12284  facwordi  12349  faclbnd5  12358  hashdom  12430  brfi1uzind  12516  ccatws1n0  12625  swrds2  12874  cjmulge0  13061  resqrtcl  13169  absge0  13202  sqreulem  13274  amgm2  13284  rlimdm  13456  rlimge0  13486  reccn2  13501  climle  13544  climserle  13567  isercoll2  13573  iseraltlem1  13586  iseralt  13589  isumclim2  13655  isumclim3  13656  isumge0  13663  fsumless  13692  cvgcmp  13712  cvgcmpce  13714  abscvgcvg  13715  isumsup2  13740  isumltss  13742  climcndslem1  13743  climcnds  13745  supcvg  13749  harmonic  13752  expcnv  13757  explecnv  13758  cvgrat  13774  mertenslem1  13775  mertenslem2  13776  clim2div  13780  ntrivcvgtail  13791  iprodclim2  13874  iprodclim3  13875  efcvg  13902  ege2le3  13907  efaddlem  13910  eftlub  13926  effsumlt  13928  tanhlt1  13977  ef01bndlem  14001  sin02gt0  14009  rpnnen2lem4  14035  ruclem2  14049  ruclem3  14050  ruclem9  14055  iddvdsexp  14091  dvdsadd  14108  dvdsfac  14125  dvdsmod  14127  3dvds  14134  divalglem1  14136  bitsfzo  14169  bitsmod  14170  bitscmp  14172  bitsinv1lem  14175  sadcaddlem  14191  sadadd3  14195  sadaddlem  14200  dvdssqim  14275  dvdsmulgcd  14276  nn0seqcvgd  14283  sqnprm  14323  mulgcddvds  14329  qredeq  14331  isprm6  14334  nonsq  14376  hashdvds  14389  prmdiv  14399  odzdvds  14406  omoe  14420  pythagtriplem4  14427  pcpre1  14450  pcdvdsb  14476  pcz  14488  pcprmpw2  14489  pcaddlem  14491  pcadd  14492  pcadd2  14493  pcmpt  14495  pcmptdvds  14497  fldivp1  14500  pcfaclem  14501  pockthlem  14507  prmreclem1  14518  prmreclem3  14520  prmreclem5  14522  prmreclem6  14523  4sqlem6  14545  4sqlem8  14547  4sqlem11  14557  4sqlem12  14558  4sqlem14  14560  4sqlem16  14562  vdwlem3  14585  vdwlem9  14591  vdwlem10  14592  vdwlem12  14594  ramub1lem2  14629  invfuc  15462  ple1  15873  eqgen  16453  lagsubg  16462  pgpfi  16824  sylow2alem2  16837  sylow2a  16838  sylow3lem4  16849  efgsrel  16951  odadd1  17053  odadd2  17054  gexex  17058  lt6abl  17096  dprd2d2  17288  dmdprdpr  17293  ablfacrp2  17313  ablfac1c  17317  pgpfaclem1  17327  ablfac2  17335  dvdsrmul1  17497  unitmulclb  17509  subrguss  17639  abvres  17683  ply1coefsupp  18531  evl1gsumadd  18589  znfld  18772  znunit  18775  frlmisfrlm  19050  matgsum  19106  pm2mpcl  19465  psmetxrge0  20983  isxmet2d  20996  mettri  21021  xmettri3  21022  mettri3  21023  xmetrtri2  21025  prdsxmetlem  21037  imasdsf1olem  21042  xblss2ps  21070  blss2ps  21072  blss2  21073  blssps  21093  blss  21094  prdsbl  21160  dscmet  21259  nmge0  21302  nmmtri  21307  nlmvscnlem2  21360  nrginvrcnlem  21365  nmoix  21402  nmoleub  21404  blcvx  21469  xrsxmet  21480  opnreen  21502  xrge0tsms  21505  icopnfcnv  21608  xrhmeo  21612  lebnumii  21632  pcophtb  21695  pi1grplem  21715  nmoleub2lem  21763  ipcau2  21843  tchcphlem1  21844  ipcau  21847  ipcnlem2  21850  rrxcph  21990  minveclem2  22007  minveclem3b  22009  pjthlem1  22018  pjthlem2  22019  ivthlem3  22031  ivth2  22033  ovolfsf  22049  ovolsslem  22061  ovollb2lem  22065  ovollb2  22066  ovolctb  22067  ovolfiniun  22078  ovolicc1  22093  ovolicc2lem4  22097  ovolicc2  22099  nulmbl2  22113  unmbl  22114  ioombl1lem4  22137  uniioombllem4  22161  uniioombllem6  22163  volivth  22182  vitalilem4  22186  itg1ge0  22259  itg1ge0a  22284  itg1lea  22285  itg1climres  22287  mbfi1fseqlem5  22292  itg2ub  22306  itg2seq  22315  itg2uba  22316  itg2splitlem  22321  itg2split  22322  itg2monolem3  22325  itg2mono  22326  itg2i1fseq2  22329  itg2addlem  22331  iblss  22377  itggt0  22414  dvferm2lem  22553  dvlip  22560  dvivthlem1  22575  dvfsumlem2  22594  dvfsumlem3  22595  ftc1lem4  22606  ply1divmo  22702  ply1remlem  22729  fta1glem2  22733  ig1pdvds  22743  plyeq0lem  22773  plydiveu  22860  fta1lem  22869  vieta1lem2  22873  aaliou3lem2  22905  aaliou3lem8  22907  ulmcn  22960  mtest  22965  itgulm  22969  radcnvlem1  22974  radcnvlt1  22979  dvradcnv  22982  pserdvlem2  22989  abelthlem2  22993  abelthlem6  22997  abelthlem7  22999  abelthlem9  23001  tangtx  23064  sinq12gt0  23066  sineq0  23080  cosordlem  23084  tanord  23091  tanregt0  23092  logrnaddcl  23128  logcj  23159  argregt0  23163  argrege0  23164  argimgt0  23165  argimlt0  23166  logimul  23167  logneg2  23168  logdivlti  23173  divlogrlim  23184  logcnlem3  23193  logcnlem4  23194  dvlog2lem  23201  logtayl  23209  rpcxpcl  23225  cxpsqrtlem  23251  cxpaddle  23294  isosctrlem1  23349  asinlem3a  23398  asinlem3  23399  asinneg  23414  asinsinlem  23419  asinsin  23420  atanlogaddlem  23441  atanlogadd  23442  atanlogsublem  23443  atanlogsub  23444  atantan  23451  atanbndlem  23453  atantayl  23465  leibpi  23470  birthdaylem3  23481  areaf  23489  cxploglim  23505  jensenlem2  23515  jensen  23516  logdiflbnd  23522  harmonicbnd4  23538  fsumharmonic  23539  wilthlem2  23541  ftalem1  23544  ftalem2  23545  ftalem5  23548  basellem6  23557  basellem8  23559  basellem9  23560  chtge0  23584  chtublem  23684  logexprlim  23698  perfectlem1  23702  bcmax  23751  bposlem1  23757  bposlem2  23758  bposlem6  23762  bposlem7  23763  lgsdilem2  23804  lgsqrlem4  23817  lgsquadlem1  23827  2sqlem3  23839  2sqlem8  23845  2sqblem  23850  chebbnd1lem2  23853  chtppilimlem1  23856  chtppilim  23858  chto1ub  23859  vmadivsum  23865  rplogsumlem1  23867  rplogsumlem2  23868  dchrisum0lem1a  23869  rpvmasumlem  23870  dchrisumlem1  23872  dchrisumlem2  23873  dchrvmasumlem2  23881  dchrisum0flblem1  23891  dchrisum0flblem2  23892  dchrisum0lem1b  23898  dchrisum0lem1  23899  dchrisum0lem2a  23900  dchrisum0lem3  23902  dchrisum0  23903  mudivsum  23913  mulogsumlem  23914  mulog2sumlem1  23917  mulog2sumlem2  23918  2vmadivsumlem  23923  chpdifbndlem1  23936  selberg3lem1  23940  selberg4lem1  23943  pntrlog2bndlem1  23960  pntrlog2bndlem2  23961  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntpbnd1a  23968  pntpbnd1  23969  pntpbnd2  23970  pntibndlem2  23974  pntibndlem3  23975  pntlemd  23977  pntlemc  23978  pntlemb  23980  pntlemg  23981  pntlemh  23982  pntlemr  23985  pntlemf  23988  pntlemo  23990  abvcxp  23998  ostth2lem1  24001  padicabv  24013  ostth2lem2  24017  ostth2lem3  24018  ostth2lem4  24019  ostth2  24020  ostth3  24021  legso  24186  krippenlem  24268  midex  24312  ttgcontlem1  24390  axpaschlem  24445  axcontlem8  24476  umgraex  24525  wwlkextproplem3  24945  clwlkisclwwlk2  24992  clwwlkndivn  25039  clwlkf1clwwlklem1  25048  ex-ind-dvds  25372  nvabs  25774  nmooge0  25880  nmoolb  25884  siii  25966  minvecolem2  25989  minvecolem4  25994  minvecolem5  25995  hlipgt0  26028  normge0  26241  normpyc  26261  pjhthlem1  26507  pjige0i  26806  nmoplb  27024  nmfnlb  27041  branmfn  27222  pjssdif2i  27291  stlei  27357  mul2lt0rgt0  27797  xlt2addrd  27809  eliccelico  27822  elicoelioo  27823  bcm1n  27834  2sqmod  27870  omndmul2  27936  archirngz  27967  archiabllem2c  27973  xrge0tsmsd  28010  ofldchr  28039  locfinreflem  28078  xrge0iifiso  28152  nexple  28239  gsumesum  28288  esumcst  28292  esumpcvgval  28307  esumcvg  28315  esumiun  28323  measssd  28423  measunl  28424  omssubadd  28508  carsgclctunlem3  28528  sibfof  28546  oddpwdc  28557  eulerpartlemgc  28565  iwrdsplit  28590  ballotlemsgt1  28713  ballotlemsel1i  28715  sgnmul  28745  signsply0  28772  signstfvc  28795  signsvtp  28804  signsvfpn  28806  zetacvg  28821  lgamgulmlem2  28836  lgamgulmlem3  28837  lgamcvg2  28861  subfaclim  28896  erdszelem7  28905  erdszelem8  28906  cvmliftlem2  28995  snmlff  29038  sinccvglem  29302  climlec3  29361  faclim  29412  dvdspw  29416  nodense  29689  nobndup  29700  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  itg2addnclem  30306  itg2addnclem3  30308  itg2gt0cn  30310  itggt0cn  30327  ftc1anclem5  30334  ftc1anclem7  30336  ftc1anclem8  30337  fnejoin1  30426  isbnd3  30520  ssbnd  30524  heiborlem8  30554  bfplem2  30559  rrncmslem  30568  rrnequiv  30571  rrntotbnd  30572  eldioph2lem1  30932  lzenom  30942  irrapxlem1  30997  irrapxlem4  31000  irrapxlem5  31001  pell14qrgt0  31034  pell1qrge1  31045  pell1qrgap  31049  pellfundge  31057  pellfundex  31061  pellfund14  31073  rmspecsqrtnq  31081  rmxypos  31124  ltrmynn0  31125  ltrmxnn0  31126  jm2.24nn  31136  jm2.17b  31138  jm2.17c  31139  jm2.24  31140  congadd  31143  congsym  31145  congneg  31146  congid  31148  mzpcong  31149  acongrep  31157  acongeq  31160  jm2.18  31169  jm2.19  31174  jm2.23  31177  jm2.25  31180  jm2.26lem3  31182  jm2.15nn0  31184  jm2.16nn0  31185  jm2.27a  31186  jm2.27c  31188  jm3.1lem1  31198  idomrootle  31393  idomsubgmo  31396  dvgrat  31434  radcnvrat  31436  dvdslcm  31445  lcmgcdlem  31453  binomcxplemnn0  31495  binomcxplemnotnn0  31502  cncmpmax  31647  zltlesub  31708  lt2addmuld  31713  fmul01  31813  fmul01lt1lem1  31817  climdivf  31857  sumnnodd  31875  dvdivbd  31959  volge0  31999  stoweidlem1  32022  stoweidlem16  32037  stoweidlem18  32039  stoweidlem24  32045  stoweidlem26  32047  stoweidlem36  32057  stoweidlem38  32059  stoweidlem41  32062  stoweidlem42  32063  stoweidlem44  32065  stoweidlem45  32066  stoweidlem48  32069  stoweidlem62  32083  wallispilem5  32090  stirlinglem1  32095  stirlinglem5  32099  stirlinglem7  32101  stirlinglem8  32102  stirlinglem9  32103  stirlinglem11  32105  fourierdlem4  32132  fourierdlem10  32138  fourierdlem37  32165  fourierdlem47  32175  fourierdlem72  32200  fourierdlem74  32202  fourierdlem79  32207  fourierdlem82  32210  fourierdlem89  32217  fourierdlem91  32219  fourierdlem93  32221  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  etransclem24  32280  etransclem25  32281  etransclem28  32284  etransclem37  32293  etransclem38  32294  etransclem44  32300  rlimdmafv  32501  2elfz2melfz  32708  usgedgleord  32791  cznnring  33018  rhmsubcrngc  33091  altgsumbcALT  33196  expnegico01  33377  flnn0div2ge  33404  rege1logbrege0  33433  fllogbd  33435  fllog2  33443  nnpw2blen  33455  nnolog2flm1  33465  dignn0ldlem  33477  dignn0flhalflem1  33490  dignn0flhalflem2  33491  lcv1  35163  lsatcv0eq  35169  lsatcvat3  35174  cvlsupr2  35465  hlatlej2  35497  cvrval4N  35535  cvratlem  35542  atcvr0eq  35547  2atlt  35560  atbtwnex  35569  athgt  35577  1cvrat  35597  ps-1  35598  hlatexch3N  35601  hlatexch4  35602  3atlem2  35605  atcvrlln2  35640  lplnexllnN  35685  4atlem3a  35718  4atlem10b  35726  4atlem11b  35729  4atlem12b  35732  2lplnja  35740  dalemply  35775  dalemsly  35776  dalem1  35780  dalem6  35789  dalem7  35790  dalem-cly  35792  dalem11  35795  dalem12  35796  dalem16  35800  dalem17  35801  dalem38  35831  dalem44  35837  dalem61  35854  lnatexN  35900  lncvrat  35903  lncmp  35904  paddasslem2  35942  dalawlem3  35994  dalawlem6  35997  dalawlem11  36002  lhpmcvr  36144  lhp2atne  36155  lhp2at0ne  36157  lautj  36214  trlval4  36310  cdlemc2  36314  cdlemc5  36317  cdleme3b  36351  cdleme11c  36383  cdleme19a  36426  cdleme20j  36441  cdleme22f  36469  cdleme23c  36474  cdleme26f2ALTN  36487  cdleme26f2  36488  cdleme35fnpq  36572  cdleme48bw  36625  cdlemg10a  36763  cdlemg11b  36765  cdlemg17g  36790  cdlemg18c  36803  cdlemi1  36941  cdlemk52  37077  dia2dimlem1  37188  dihord1  37342  dihjatcclem4  37545  inductionexd  38419  imo72b2  38445
  Copyright terms: Public domain W3C validator