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

Theorem breqtrd 4461
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 4449 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 210 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  breqtrrd  4463  syl5breq  4472  domunsn  7669  mapdom2  7690  phplem4  7701  mapfien2  7870  wemaplem2  7975  infdifsn  8076  cantnff  8096  infxpenlem  8394  pwcda1  8577  pwcdadom  8599  infmap2  8601  ssfin4  8693  canthp1lem1  9033  nqereq  9316  ltexnq  9356  ltbtwnnq  9359  add20  10071  mullt0  10079  ltm1  10389  recgt0  10393  prodgt0  10394  prodge0  10396  ltmul1a  10398  mulge0b  10419  recp1lt1  10450  recreclt  10451  ledivp1  10454  ledivp1i  10478  ltdivp1i  10479  ltaddrp2d  11297  xleadd1a  11456  xov1plusxeqvd  11677  fz01en  11724  fzonmapblen  11850  fladdz  11940  flhalf  11944  fldiv  11969  modsubdir  12037  fzen2  12061  serle  12144  ltexp2a  12199  leexp2a  12203  exple1  12207  expubnd  12208  bernneq  12274  expmulnbnd  12280  discr1  12284  discr  12285  faclbnd6  12359  hashfz  12467  hashfun  12477  seqcoll  12494  sqeqd  12981  sqrlem7  13064  sqrtge0  13073  sqrtneglem  13082  abslt  13129  absle  13130  abstri  13145  rlimge0  13386  reccn2  13401  climaddc2  13440  isercolllem1  13469  caucvgrlem  13477  summolem2a  13519  isumge0  13563  fsumle  13595  fsumlt  13596  o1fsum  13609  supcvg  13649  expcnv  13657  geolim  13661  geolim2  13662  georeclim  13663  geo2lim  13666  mertenslem1  13675  mertens  13677  prodmolem2a  13723  efcllem  13795  ef0lem  13796  efgt0  13820  eftlub  13826  eflt  13834  sinbnd  13897  cosbnd  13898  ef01bndlem  13901  sin01gt0  13907  cos01gt0  13908  sin02gt0  13909  eirrlem  13919  rpnnen2lem11  13940  rpnnen2  13941  ruclem11  13955  dvdssub2  14005  dvdsadd2b  14010  dvdsexp  14024  3dvds  14032  bitsfzolem  14066  bitsinv1lem  14073  bezoutlem4  14161  dvdsgcd  14163  dvdsmulgcd  14174  nn0seqcvgd  14181  prmind2  14210  rpmulgcd2  14228  qredeq  14229  rpdvds  14247  divdenle  14264  hashdvds  14287  phimullem  14291  eulerthlem2  14294  prmdiveq  14298  prmdivdiv  14299  opoe  14317  pythagtriplem4  14325  pythagtriplem10  14326  pythagtriplem19  14339  iserodd  14341  pcpre1  14348  pcadd2  14391  qexpz  14402  expnprm  14403  pockthlem  14405  prmreclem2  14417  prmreclem3  14418  4sqlem7  14444  4sqlem10  14447  4sqlem11  14455  4sqlem12  14456  4sqlem14  14458  4sqlem15  14459  4sqlem16  14460  0ram  14520  ffthiso  15277  latmlej12  15700  qusgrp  16235  pgpfi1  16594  sylow1lem4  16600  sylow1lem5  16601  odcau  16603  pgpfi  16604  pgpssslw  16613  sylow3lem4  16629  sylow3lem6  16631  efgsfo  16736  frgp0  16757  odadd1  16833  odadd2  16834  odadd  16835  gexexlem  16837  lt6abl  16876  gsumzsubmcl  16907  pwsgsum  16988  dprd2dlem1  17069  dprd2d2  17072  ablfacrplem  17095  ablfacrp  17096  ablfacrp2  17097  ablfac1b  17100  ablfac1eu  17103  pgpfac1lem3a  17106  ablfaclem2  17116  dvdsrid  17279  dvdsrtr  17280  dvdsrneg  17282  unitmulcl  17292  unitgrp  17295  unitnegcl  17309  isdrng2  17385  subrguss  17423  subrgunit  17426  abvsubtri  17463  fidomndrnglem  17934  psrbaglesupp  17996  psrbaglesuppOLD  17997  gzrngunit  18462  prmirredlem  18501  prmirredlemOLD  18504  znidomb  18578  frlmgsum  18780  invrvald  19156  psmetsym  20792  psmettri  20793  mettri2  20822  xmetsym  20828  xmettri  20832  prdsxmetlem  20849  xblss2ps  20882  xblss2  20883  blhalf  20886  xmsge0  20944  ngptgp  21128  nrginvrcnlem  21177  nmoeq0  21221  cnmet  21257  blcvx  21281  opnreen  21314  metdcnlem  21319  metdstri  21333  metdsle  21334  metnrmlem1  21341  metnrmlem3  21343  lebnumlem1  21439  pi1inv  21530  cphnmf  21620  ipge0  21623  ipcau2  21655  tchcphlem1  21656  csbren  21804  minveclem2  21819  minveclem3  21822  ovolssnul  21876  ovolctb  21879  ovolunnul  21889  ovoliunlem1  21891  ovoliun2  21895  ovoliunnul  21896  ioombl1lem4  21949  uniioombllem3  21972  uniioombllem4  21973  uniioombllem5  21974  uniioombl  21976  volcn  21993  vitalilem2  21996  vitalilem5  21999  itg1lea  22097  mbfi1fseqlem6  22105  mbfi1flimlem  22107  itg2eqa  22130  itg2splitlem  22133  itg2split  22134  itg2monolem1  22135  itg2cnlem2  22147  iblabsr  22214  iblmulc2  22215  dveflem  22358  dvef  22359  dvferm2lem  22365  dvlip  22372  c1liplem1  22375  dveq0  22379  dvlt0  22384  dvivthlem1  22387  lhop1  22393  dvfsumle  22400  dvfsumlem4  22408  dvfsumrlim3  22412  dvfsum2  22413  ftc1a  22416  ftc1lem4  22418  deg1add  22482  ply1divex  22515  ply1rem  22542  fta1glem2  22545  fta1blem  22547  ig1pdvds  22555  plyeq0lem  22585  dgrcolem2  22649  plydivlem4  22670  plyrem  22679  fta1lem  22681  aalioulem3  22708  aaliou2b  22715  aaliou3lem3  22718  aaliou3lem8  22719  ulmcn  22772  ulmdvlem1  22773  itgulm  22781  pserulm  22795  pserdvlem2  22801  abelthlem2  22805  abelthlem5  22808  abelthlem6  22809  abelthlem7  22811  abelthlem8  22812  abelthlem9  22813  sinq12gt0  22878  sinq34lt0t  22880  cosq14gt0  22881  cosq14ge0  22882  efif1olem3  22909  argimgt0  22975  argimlt0  22976  logneg2  22978  logcnlem3  23003  logcnlem4  23004  logtayllem  23018  logtayl2  23021  cxpsqrtlem  23061  cxpsqrt  23062  cxpaddlelem  23103  abscxpbnd  23105  loglesqrt  23110  ang180lem2  23120  atanlogaddlem  23222  atanlogsublem  23224  atantan  23232  atans2  23240  atantayl  23246  leibpi  23251  log2tlbnd  23254  birthdaylem2  23260  birthdaylem3  23261  cxp2limlem  23283  jensenlem2  23295  jensen  23296  logdiflbnd  23302  emcllem2  23304  emcllem4  23306  harmonicbnd4  23318  fsumharmonic  23319  wilthlem3  23322  basellem1  23332  basellem3  23334  basellem4  23335  fsumdvdsdiaglem  23437  dvdsppwf1o  23440  dvdsmulf1o  23448  chteq0  23462  chtub  23465  chpub  23473  logfacubnd  23474  logfaclbnd  23475  logexprlim  23478  perfectlem2  23483  dchrfi  23508  bclbnd  23533  bposlem1  23537  bposlem3  23539  bposlem4  23540  bposlem6  23542  lgslem1  23549  lgsqrlem2  23595  lgsqrlem4  23597  lgseisenlem2  23603  lgsquadlem1  23607  lgsquadlem2  23608  lgsquad2lem1  23611  2sqlem3  23619  2sqlem4  23620  2sqlem8  23625  2sqlem11  23628  chebbnd1lem2  23633  chebbnd1lem3  23634  chtppilimlem1  23636  chpchtlim  23642  vmadivsum  23645  vmadivsumb  23646  rpvmasumlem  23650  dchrisumlem2  23653  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumlem3  23662  dchrisum0flblem2  23672  dchrisum0fno1  23674  dchrisum0re  23676  dchrisum0lem1  23679  dchrisum0lem2a  23680  mudivsum  23693  mulogsumlem  23694  mulog2sumlem2  23698  vmalogdivsum2  23701  selberglem2  23709  selbergb  23712  selberg2b  23715  logdivbnd  23719  selberg3lem1  23720  selberg3lem2  23721  selberg4lem1  23723  pntrmax  23727  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6a  23745  pntrlog2bndlem6  23746  pntrlog2bnd  23747  pntpbnd1a  23748  pntpbnd1  23749  pntpbnd2  23750  pntibndlem1  23752  pntibndlem2  23754  pntlemb  23760  pntlemq  23764  pntlemr  23765  pntlemj  23766  pntlemk  23769  qabvle  23788  padicabvcxp  23795  ostth2lem2  23797  ostth2lem3  23798  ostth2lem4  23799  ostth3  23801  legtrid  23956  legov3  23962  krippenlem  24045  mideulem2  24086  midex  24089  opphllem5  24101  opphllem6  24102  opphl  24103  lmieu  24128  lmiisolem  24139  ttgcontlem1  24166  colinearalglem4  24190  axpaschlem  24221  axcontlem7  24251  clwlkndivn  24831  nvge0  25555  smcnlem  25585  nmoub3i  25666  nmoub2i  25667  nmlno0lem  25686  minvecolem2  25769  htthlem  25812  norm3dif2  26046  bcs2  26077  chscllem2  26534  eigposi  26733  nmopub2tALT  26806  nmfnleub2  26823  nmlnop0iALT  26892  riesz1  26962  cnlnadjlem2  26965  nmopcoadji  26998  leopsq  27026  leopmul  27031  leopnmid  27035  nmopleid  27036  opsqrlem6  27042  0leopj  27083  hstle1  27123  strlem3a  27149  mdslmd4i  27230  cvexchlem  27265  cdj1i  27330  mul2lt0bi  27547  le2halvesd  27554  xlt2addrd  27556  2sqcoprm  27613  2sqmod  27614  archiabllem1a  27713  archiabllem2a  27716  archiabllem2c  27717  xrge0tsmsd  27753  orngsqr  27772  ornglmulle  27773  orngrmulle  27774  orng0le1  27780  metideq  27850  metider  27851  sqsscirc1  27868  esumle  28043  esummono  28044  esumlef  28048  esumcst  28049  aean  28194  dya2ub  28219  dya2icoseg  28226  eulerpartlemb  28285  fibp1  28318  sgnmulsgp  28467  eluzmn  28469  signsplypnf  28485  signsply0  28486  lgamgulmlem2  28550  lgamgulm2  28556  lgambdd  28557  lgamucov  28558  lgamcvglem  28560  lgamcvg2  28575  gamcvg  28576  subfacval3  28611  sconpht2  28661  sconpi1  28662  rescon  28669  snmlff  28752  sinccvglem  29016  faclimlem2  29145  btwnouttr2  29648  ltflcei  30019  heicant  30025  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  volsupnfl  30035  dvtanlem  30040  itg2addnclem  30042  itg2addnclem3  30044  iblmulc2nc  30056  bddiblnc  30061  ftc1cnnclem  30064  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc2nc  30075  dvasin  30079  geomcau  30228  bfplem2  30295  rrncmslem  30304  rrnequiv  30307  irrapxlem1  30734  pell1qrgaplem  30785  pell1qrgap  30786  monotoddzzfi  30854  jm2.24nn  30873  congtr  30879  congmul  30881  congsub  30884  fzmaxdif  30895  acongeq  30897  bezoutr1  30900  jm2.20nn  30915  jm2.25  30917  mapfien2OLD  31018  hbtlem4  31051  dgrsub2  31060  mpaaeu  31075  idomsubgmo  31131  cvgdvgrat  31170  radcnvrat  31171  hashnzfzclim  31203  dvconstbi  31215  mulltgt0  31351  oddfl  31413  2timesgt  31429  lt3addmuld  31455  lt4addmuld  31460  iccshift  31512  iooshift  31516  fsumnncl  31526  fmul01  31528  fmul01lt1lem1  31532  fmul01lt1lem2  31533  mccllem  31559  climrec  31563  climexp  31565  climneg  31570  limcrecl  31589  sumnnodd  31590  lptioo2  31591  lptioo1  31592  ltmod  31598  lptre2pt  31600  0ellimcdiv  31609  limclner  31611  cncficcgt0  31645  cncfioobdlem  31653  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvdsn1add  31690  dvnxpaek  31693  dvnmul  31694  dvnprodlem1  31697  itgiccshift  31733  itgperiod  31734  stoweidlem1  31737  stoweidlem11  31747  stoweidlem13  31749  stoweidlem26  31762  stoweidlem34  31770  stoweidlem38  31774  stoweidlem42  31778  stoweidlem51  31787  stoweidlem59  31795  stirlinglem5  31814  stirlinglem6  31815  stirlinglem7  31816  stirlinglem10  31819  stirlinglem11  31820  stirlinglem13  31822  stirlinglem15  31824  dirkercncflem1  31839  dirkercncflem4  31842  fourierdlem4  31847  fourierdlem10  31853  fourierdlem11  31854  fourierdlem15  31858  fourierdlem20  31863  fourierdlem25  31868  fourierdlem26  31869  fourierdlem30  31873  fourierdlem37  31880  fourierdlem39  31882  fourierdlem40  31883  fourierdlem41  31884  fourierdlem42  31885  fourierdlem44  31887  fourierdlem47  31890  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem51  31894  fourierdlem52  31895  fourierdlem54  31897  fourierdlem60  31903  fourierdlem61  31904  fourierdlem63  31906  fourierdlem64  31907  fourierdlem65  31908  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem78  31921  fourierdlem79  31922  fourierdlem81  31924  fourierdlem84  31927  fourierdlem87  31930  fourierdlem92  31935  fourierdlem93  31936  fourierdlem101  31944  fourierdlem102  31945  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem114  31957  sqwvfoura  31965  sqwvfourb  31966  fouriersw  31968  etransclem19  31990  etransclem23  31994  etransclem24  31995  etransclem25  31996  etransclem27  31998  etransclem28  31999  etransclem32  32003  etransclem35  32006  etransclem37  32008  etransclem48  32019  isosctrlem1ALT  33602  lsatcvatlem  34649  islshpcv  34653  atlatmstc  34919  cvlsupr7  34948  cvrval3  35012  cvrval5  35014  cvrexchlem  35018  atcvrj1  35030  cvrat3  35041  cvrat4  35042  atbtwn  35045  1cvratex  35072  hlatexch4  35080  3atlem1  35082  3atlem2  35083  atcvrlln2  35118  atcvrlln  35119  lplnllnneN  35155  llncvrlpln2  35156  4atlem3b  35197  lplncvrlvol2  35214  dalemswapyz  35255  dalemswapyzps  35289  dalem25  35297  dalem39  35310  dalem58  35329  dalem59  35330  lneq2at  35377  lncvrat  35381  dalawlem2  35471  dalawlem3  35472  dalawlem4  35473  dalawlem6  35475  dalawlem9  35478  dalawlem11  35480  dalawlem12  35481  lhpocnle  35615  lhpmcvr3  35624  lhpmcvr5N  35626  lhpmcvr6N  35627  4atexlemunv  35665  4atexlemc  35668  4atexlemex2  35670  lautm  35693  cdlemc2  35792  cdleme5  35840  cdleme11j  35867  cdleme16b  35879  cdlemednpq  35899  cdleme19e  35908  cdleme20i  35918  cdleme22a  35941  cdleme22cN  35943  cdleme22d  35944  cdleme22e  35945  cdleme22eALTN  35946  cdleme22f  35947  cdleme23c  35952  cdleme30a  35979  cdleme35a  36049  cdleme35b  36051  cdleme42h  36083  cdlemeg46rgv  36129  cdlemg8b  36229  cdlemg12e  36248  cdlemg13a  36252  cdlemg17pq  36273  cdlemg18c  36281  cdlemg19  36285  cdlemg21  36287  cdlemg31d  36301  cdlemg33a  36307  tendoid  36374  cdlemk4  36435  cdlemki  36442  cdlemk10  36444  cdlemksv2  36448  cdlemk12  36451  cdlemk14  36455  cdlemk15  36456  cdlemk1u  36460  cdlemk5u  36462  cdlemk12u  36473  cdlemk45  36548  cdlemk48  36551  dia2dimlem1  36666  dia2dimlem2  36667  dia2dimlem3  36668  cdlemm10N  36720  cdlemn2  36797  dihjustlem  36818  dihglbcpreN  36902  dihmeetlem3N  36907
  Copyright terms: Public domain W3C validator