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

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

Proof of Theorem breqtrd
StepHypRef Expression
1 breqtrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32breq2d 4378 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 213 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367
This theorem is referenced by:  breqtrrd  4393  syl5breq  4402  domunsn  7675  mapdom2  7696  phplem4  7707  mapfien2  7875  wemaplem2  8015  infdifsn  8114  cantnff  8131  infxpenlem  8396  pwcda1  8575  pwcdadom  8597  infmap2  8599  ssfin4  8691  canthp1lem1  9028  nqereq  9311  ltexnq  9351  ltbtwnnq  9354  add20  10077  mullt0  10084  ltm1  10396  recgt0  10400  prodgt0  10401  prodge0  10403  ltmul1a  10405  mulge0b  10426  recp1lt1  10455  recreclt  10456  ledivp1  10459  ledivp1i  10483  ltdivp1i  10484  ltaddrp2d  11323  mul2lt0bi  11353  xleadd1a  11490  xov1plusxeqvd  11729  fz01en  11778  fzonmapblen  11912  fladdz  12008  flhalf  12012  fldiv  12037  modsubdir  12108  fzen2  12132  serle  12218  ltexp2a  12274  leexp2a  12278  exple1  12282  expubnd  12283  bernneq  12348  expmulnbnd  12354  discr1  12358  discr  12359  faclbnd6  12434  hashfz  12547  hashfun  12557  seqcoll  12575  sqeqd  13173  sqrlem7  13256  sqrtge0  13265  sqrtneglem  13274  abslt  13321  absle  13322  abstri  13337  rlimge0  13588  reccn2  13603  climaddc2  13642  isercolllem1  13671  caucvgrlem  13679  caucvgrlemOLD  13680  summolem2a  13724  isumge0  13770  fsumle  13802  fsumlt  13803  o1fsum  13816  supcvg  13857  expcnv  13865  geolim  13869  geolim2  13870  georeclim  13871  geo2lim  13874  mertenslem1  13883  mertens  13885  prodmolem2a  13931  efcllem  14075  ef0lem  14076  efgt0  14100  eftlub  14106  eflt  14114  sinbnd  14177  cosbnd  14178  ef01bndlem  14181  sin01gt0  14187  cos01gt0  14188  sin02gt0  14189  eirrlem  14199  rpnnen2lem11  14220  rpnnen2  14221  ruclem11  14235  dvdssub2  14285  dvdsadd2b  14290  dvdsexp  14304  3dvds  14312  bitsfzolem  14350  bitsfzolemOLD  14351  bitsinv1lem  14358  bezoutlem4OLD  14449  bezoutlem4  14452  dvdsgcd  14454  dvdsmulgcd  14465  nn0seqcvgd  14472  prmind2  14578  rpmulgcd2  14605  qredeq  14606  rpdvds  14619  divdenle  14641  hashdvds  14666  phimullem  14670  eulerthlem2  14673  prmdiveq  14677  prmdivdiv  14678  opoe  14704  pythagtriplem4  14712  pythagtriplem10  14713  pythagtriplem19  14726  iserodd  14728  pcpre1  14735  pcadd2  14778  qexpz  14789  expnprm  14790  pockthlem  14792  prmreclem2  14804  prmreclem3  14805  4sqlem7  14831  4sqlem10  14834  4sqlem11  14842  4sqlem12  14843  4sqlem14OLD  14845  4sqlem15OLD  14846  4sqlem16OLD  14847  4sqlem14  14851  4sqlem15  14852  4sqlem16  14853  0ram  14921  ffthiso  15777  latmlej12  16280  qusgrp  16815  pgpfi1  17190  sylow1lem4  17196  sylow1lem5  17197  odcau  17199  pgpfi  17200  pgpssslw  17209  sylow3lem4  17225  sylow3lem6  17227  efgsfo  17332  frgp0  17353  odadd1  17429  odadd2  17430  odadd  17431  gexexlem  17433  lt6abl  17472  gsumzsubmcl  17494  pwsgsum  17554  dprd2dlem1  17617  dprd2d2  17620  ablfacrplem  17641  ablfacrp  17642  ablfacrp2  17643  ablfac1b  17646  ablfac1eu  17649  pgpfac1lem3a  17652  ablfaclem2  17662  dvdsrid  17822  dvdsrtr  17823  dvdsrneg  17825  unitmulcl  17835  unitgrp  17838  unitnegcl  17852  isdrng2  17928  subrguss  17966  subrgunit  17969  abvsubtri  18006  fidomndrnglem  18473  psrbaglesupp  18535  gzrngunit  18976  prmirredlem  19006  znidomb  19074  frlmgsum  19272  invrvald  19643  psmetsym  21268  psmettri  21269  mettri2  21298  xmetsym  21304  xmettri  21308  prdsxmetlem  21325  xblss2ps  21358  xblss2  21359  blhalf  21362  xmsge0  21420  ngptgp  21586  nrginvrcnlem  21635  nmoeq0  21699  cnmet  21734  blcvx  21758  opnreen  21791  metdcnlem  21796  metdstri  21810  metdsle  21811  metnrmlem1  21818  metnrmlem3  21820  metdstriOLD  21825  metdsleOLD  21826  metnrmlem1OLD  21833  metnrmlem3OLD  21835  lebnumlem1  21931  lebnumlem1OLD  21934  pi1inv  22025  cphnmf  22115  ipge0  22118  ipcau2  22150  tchcphlem1  22151  csbren  22295  minveclem2  22310  minveclem3  22313  minveclem2OLD  22322  minveclem3OLD  22325  ovolssnul  22382  ovolctb  22385  ovolunnul  22395  ovoliunlem1  22397  ovoliun2  22401  ovoliunnul  22402  ioombl1lem4  22456  uniioombllem3  22485  uniioombllem4  22486  uniioombllem5  22487  uniioombl  22489  volcn  22506  vitalilem2  22509  vitalilem5  22512  itg1lea  22612  mbfi1fseqlem6  22620  mbfi1flimlem  22622  itg2eqa  22645  itg2splitlem  22648  itg2split  22649  itg2monolem1  22650  itg2cnlem2  22662  iblabsr  22729  iblmulc2  22730  dveflem  22873  dvef  22874  dvferm2lem  22880  dvlip  22887  c1liplem1  22890  dveq0  22894  dvlt0  22899  dvivthlem1  22902  lhop1  22908  dvfsumle  22915  dvfsumlem4  22923  dvfsumrlim3  22927  dvfsum2  22928  ftc1a  22931  ftc1lem4  22933  deg1add  22994  ply1divex  23029  ply1rem  23056  fta1glem2  23059  fta1blem  23061  ig1pdvds  23070  ig1pdvdsOLD  23076  plyeq0lem  23106  dgrcolem2  23170  plydivlem4  23191  plyrem  23200  fta1lem  23202  aalioulem3  23232  aaliou2b  23239  aaliou3lem3  23242  aaliou3lem8  23243  ulmcn  23296  ulmdvlem1  23297  itgulm  23305  pserulm  23319  pserdvlem2  23325  abelthlem2  23329  abelthlem5  23332  abelthlem6  23333  abelthlem7  23335  abelthlem8  23336  abelthlem9  23337  sinq12gt0  23404  sinq34lt0t  23406  cosq14gt0  23407  cosq14ge0  23408  efif1olem3  23435  argimgt0  23503  argimlt0  23504  logneg2  23506  logcnlem3  23531  logcnlem4  23532  logtayllem  23546  logtayl2  23549  cxpsqrtlem  23589  cxpsqrt  23590  cxpaddlelem  23633  abscxpbnd  23635  loglesqrt  23640  ang180lem2  23681  atanlogaddlem  23781  atanlogsublem  23783  atantan  23791  atans2  23799  atantayl  23805  leibpi  23810  log2tlbnd  23813  birthdaylem2  23820  birthdaylem3  23821  cxp2limlem  23843  jensenlem2  23855  jensen  23856  logdiflbnd  23862  emcllem2  23864  emcllem4  23866  harmonicbnd4  23878  fsumharmonic  23879  lgamgulmlem2  23897  lgamgulm2  23903  lgambdd  23904  lgamucov  23905  lgamcvglem  23907  lgamcvg2  23922  gamcvg  23923  wilthlem3  23937  basellem1  23949  basellem3  23951  basellem4  23952  fsumdvdsdiaglem  24054  dvdsppwf1o  24057  dvdsmulf1o  24065  chteq0  24079  chtub  24082  chpub  24090  logfacubnd  24091  logfaclbnd  24092  logexprlim  24095  perfectlem2  24100  dchrfi  24125  bclbnd  24150  bposlem1  24154  bposlem3  24156  bposlem4  24157  bposlem6  24159  lgslem1  24166  lgsqrlem2  24212  lgsqrlem4  24214  lgseisenlem2  24220  lgsquadlem1  24224  lgsquadlem2  24225  lgsquad2lem1  24228  2sqlem3  24236  2sqlem4  24237  2sqlem8  24242  2sqlem11  24245  chebbnd1lem2  24250  chebbnd1lem3  24251  chtppilimlem1  24253  chpchtlim  24259  vmadivsum  24262  vmadivsumb  24263  rpvmasumlem  24267  dchrisumlem2  24270  dchrmusum2  24274  dchrvmasumlem2  24278  dchrvmasumlem3  24279  dchrisum0flblem2  24289  dchrisum0fno1  24291  dchrisum0re  24293  dchrisum0lem1  24296  dchrisum0lem2a  24297  mudivsum  24310  mulogsumlem  24311  mulog2sumlem2  24315  vmalogdivsum2  24318  selberglem2  24326  selbergb  24329  selberg2b  24332  logdivbnd  24336  selberg3lem1  24337  selberg3lem2  24338  selberg4lem1  24340  pntrmax  24344  pntrlog2bndlem2  24358  pntrlog2bndlem3  24359  pntrlog2bndlem5  24361  pntrlog2bndlem6a  24362  pntrlog2bndlem6  24363  pntrlog2bnd  24364  pntpbnd1a  24365  pntpbnd1  24366  pntpbnd2  24367  pntibndlem1  24369  pntibndlem2  24371  pntlemb  24377  pntlemq  24381  pntlemr  24382  pntlemj  24383  pntlemk  24386  qabvle  24405  padicabvcxp  24412  ostth2lem2  24414  ostth2lem3  24415  ostth2lem4  24416  ostth3  24418  legtrid  24578  legov3  24585  krippenlem  24677  mideulem2  24718  midex  24721  opphllem5  24735  opphllem6  24736  opphl  24738  lmieu  24768  lmiisolem  24780  ttgcontlem1  24857  colinearalglem4  24881  axpaschlem  24912  axcontlem7  24942  clwlkndivn  25523  nvge0  26245  smcnlem  26275  nmoub3i  26356  nmoub2i  26357  nmlno0lem  26376  minvecolem2  26459  minvecolem2OLD  26469  htthlem  26512  norm3dif2  26746  bcs2  26777  chscllem2  27233  eigposi  27431  nmopub2tALT  27504  nmfnleub2  27521  nmlnop0iALT  27590  riesz1  27660  cnlnadjlem2  27663  nmopcoadji  27696  leopsq  27724  leopmul  27729  leopnmid  27733  nmopleid  27734  opsqrlem6  27740  0leopj  27781  hstle1  27821  strlem3a  27847  mdslmd4i  27928  cvexchlem  27963  cdj1i  28028  le2halvesd  28285  xlt2addrd  28288  2sqcoprm  28359  2sqmod  28360  archiabllem1a  28459  archiabllem2a  28462  archiabllem2c  28463  xrge0tsmsd  28500  orngsqr  28519  ornglmulle  28520  orngrmulle  28521  orng0le1  28527  fzto1st1  28567  metideq  28648  metider  28649  sqsscirc1  28666  esummono  28827  esumpad2  28829  esumle  28831  esumlef  28835  esumcst  28836  esumrnmpt2  28841  esum2d  28866  aean  29019  dya2ub  29044  dya2icoseg  29051  omssubadd  29080  omssubaddlemOLD  29083  omssubaddOLD  29084  inelcarsg  29095  carsgsigalem  29099  carsggect  29102  carsgclctunlem2  29103  eulerpartlemb  29153  fibp1  29186  sgnmulsgp  29373  eluzmn  29375  signsplypnf  29391  signsply0  29392  subfacval3  29864  sconpht2  29913  sconpi1  29914  rescon  29921  snmlff  30004  sinccvglem  30268  faclimlem2  30331  btwnouttr2  30738  ltflcei  31840  poimirlem9  31856  poimirlem26  31873  poimirlem27  31874  poimirlem29  31876  heicant  31882  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  volsupnfl  31892  dvtanlemOLD  31898  itg2addnclem  31900  itg2addnclem3  31902  iblmulc2nc  31914  bddiblnc  31919  ftc1cnnclem  31922  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  ftc2nc  31933  dvasin  31935  geomcau  31995  bfplem2  32062  rrncmslem  32071  rrnequiv  32074  lsatcvatlem  32527  islshpcv  32531  atlatmstc  32797  cvlsupr7  32826  cvrval3  32890  cvrval5  32892  cvrexchlem  32896  atcvrj1  32908  cvrat3  32919  cvrat4  32920  atbtwn  32923  1cvratex  32950  hlatexch4  32958  3atlem1  32960  3atlem2  32961  atcvrlln2  32996  atcvrlln  32997  lplnllnneN  33033  llncvrlpln2  33034  4atlem3b  33075  lplncvrlvol2  33092  dalemswapyz  33133  dalemswapyzps  33167  dalem25  33175  dalem39  33188  dalem58  33207  dalem59  33208  lneq2at  33255  lncvrat  33259  dalawlem2  33349  dalawlem3  33350  dalawlem4  33351  dalawlem6  33353  dalawlem9  33356  dalawlem11  33358  dalawlem12  33359  lhpocnle  33493  lhpmcvr3  33502  lhpmcvr5N  33504  lhpmcvr6N  33505  4atexlemunv  33543  4atexlemc  33546  4atexlemex2  33548  lautm  33571  cdlemc2  33670  cdleme5  33718  cdleme11j  33745  cdleme16b  33757  cdlemednpq  33777  cdleme19e  33786  cdleme20i  33796  cdleme22a  33819  cdleme22cN  33821  cdleme22d  33822  cdleme22e  33823  cdleme22eALTN  33824  cdleme22f  33825  cdleme23c  33830  cdleme30a  33857  cdleme35a  33927  cdleme35b  33929  cdleme42h  33961  cdlemeg46rgv  34007  cdlemg8b  34107  cdlemg12e  34126  cdlemg13a  34130  cdlemg17pq  34151  cdlemg18c  34159  cdlemg19  34163  cdlemg21  34165  cdlemg31d  34179  cdlemg33a  34185  tendoid  34252  cdlemk4  34313  cdlemki  34320  cdlemk10  34322  cdlemksv2  34326  cdlemk12  34329  cdlemk14  34333  cdlemk15  34334  cdlemk1u  34338  cdlemk5u  34340  cdlemk12u  34351  cdlemk45  34426  cdlemk48  34429  dia2dimlem1  34544  dia2dimlem2  34545  dia2dimlem3  34546  cdlemm10N  34598  cdlemn2  34675  dihjustlem  34696  dihglbcpreN  34780  dihmeetlem3N  34785  irrapxlem1  35579  pell1qrgaplem  35632  pell1qrgap  35633  monotoddzzfi  35703  jm2.24nn  35722  congtr  35728  congmul  35730  congsub  35733  fzmaxdif  35744  acongeq  35746  bezoutr1  35749  jm2.20nn  35765  jm2.25  35767  hbtlem4  35898  dgrsub2  35907  mpaaeu  35929  idomsubgmo  35985  int-sqgeq0d  36546  int-ineqmvtd  36551  cvgdvgrat  36575  radcnvrat  36576  hashnzfzclim  36584  dvconstbi  36596  binomcxplemdvbinom  36615  isosctrlem1ALT  37247  mulltgt0  37259  oddfl  37384  2timesgt  37398  lt3addmuld  37416  lt4addmuld  37421  supxrgere  37453  supxrgelem  37457  supxrge  37458  xadd0ge2  37461  infrpge  37471  xrlexaddrp  37472  xralrple2  37474  iccshift  37511  iooshift  37515  fsumnncl  37534  fmul01  37541  fmul01lt1lem1  37545  fmul01lt1lem2  37546  mccllem  37560  climrec  37564  climexp  37566  climneg  37572  limcrecl  37592  sumnnodd  37593  lptioo2  37594  lptioo1  37595  ltmod  37601  lptre2pt  37603  0ellimcdiv  37613  limclner  37615  cncficcgt0  37649  cncfioobdlem  37657  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvdsn1add  37697  dvnxpaek  37700  dvnmul  37701  dvnprodlem1  37704  itgiccshift  37740  itgperiod  37741  stoweidlem1  37744  stoweidlem11  37754  stoweidlem13  37756  stoweidlem26  37769  stoweidlem34  37778  stoweidlem38  37782  stoweidlem42  37786  stoweidlem51  37795  stoweidlem59  37803  stirlinglem5  37823  stirlinglem6  37824  stirlinglem7  37825  stirlinglem10  37828  stirlinglem11  37829  stirlinglem13  37831  stirlinglem15  37833  dirkercncflem1  37848  dirkercncflem4  37851  fourierdlem4  37856  fourierdlem10  37862  fourierdlem11  37863  fourierdlem15  37867  fourierdlem20  37872  fourierdlem25  37877  fourierdlem26  37878  fourierdlem30  37882  fourierdlem37  37890  fourierdlem39  37892  fourierdlem40  37893  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem44  37898  fourierdlem47  37900  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem51  37904  fourierdlem52  37905  fourierdlem54  37907  fourierdlem60  37913  fourierdlem61  37914  fourierdlem63  37916  fourierdlem64  37917  fourierdlem65  37918  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem78  37931  fourierdlem79  37932  fourierdlem81  37934  fourierdlem84  37937  fourierdlem87  37940  fourierdlem92  37945  fourierdlem93  37946  fourierdlem101  37954  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fourierdlem114  37967  sqwvfoura  37975  sqwvfourb  37976  fouriersw  37978  etransclem19  38001  etransclem23  38005  etransclem24  38006  etransclem25  38007  etransclem27  38009  etransclem32  38014  etransclem35  38017  etransclem48OLD  38030  etransclem48  38031  fsumlesge0  38070  sge0cl  38074  sge0supre  38082  sge0less  38085  sge0gerp  38088  sge0ltfirp  38093  sge0le  38100  sge0ltfirpmpt  38101  sge0split  38102  sge0rpcpnf  38114  sge0ltfirpmpt2  38119  sge0isum  38120  sge0xaddlem1  38126  sge0pnffigtmpt  38133  sge0pnffsumgt  38135  sge0gtfsumgt  38136  nnfoctbdjlem  38144  meassle  38152  omeiunle  38189  omeiunltfirp  38191  carageniuncllem2  38194  carageniuncl  38195  hoicvr  38217  ovnlerp  38231  ovnsubaddlem1  38239  hsphoidmvle2  38254  hoidmv1lelem2  38261  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem5  38268  ovnhoilem2  38271  ovnhoi  38272  perfectALTVlem2  38657  nnpw2blen  39994
  Copyright terms: Public domain W3C validator