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

Theorem breqtrd 4049
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 4037 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 201 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625   class class class wbr 4025
This theorem is referenced by:  breqtrrd  4051  syl5breq  4060  domunsn  7013  mapdom2  7034  phplem4  7045  wemaplem2  7264  infdifsn  7359  cantnff  7377  infxpenlem  7643  pwcda1  7822  pwcdadom  7844  infmap2  7846  ssfin4  7938  canthp1lem1  8276  nqereq  8561  ltexnq  8601  ltbtwnnq  8604  add20  9288  mullt0  9295  ltm1  9598  recgt0  9602  prodgt0  9603  prodge0  9605  ltmul1a  9607  recp1lt1  9656  recreclt  9657  ledivp1  9660  ledivp1i  9684  ltdivp1i  9685  ltaddrp2d  10422  xleadd1a  10575  xov1plusxeqvd  10782  fz01en  10820  fladdz  10952  flhalf  10956  fldiv  10966  modsubdir  11010  fzen2  11033  serle  11103  ltexp2a  11155  leexp2a  11159  exple1  11163  expubnd  11164  bernneq  11229  expmulnbnd  11235  discr1  11239  discr  11240  faclbnd6  11314  hashfz  11383  hashfun  11391  seqcoll  11403  sqeqd  11653  sqrlem7  11736  sqrge0  11745  sqrneglem  11754  abslt  11800  absle  11801  abstri  11816  rlimge0  12057  reccn2  12072  climaddc2  12111  isercolllem1  12140  caucvgrlem  12147  summolem2a  12190  isumge0  12231  fsumle  12259  fsumlt  12260  o1fsum  12273  supcvg  12316  expcnv  12324  geolim  12328  geolim2  12329  georeclim  12330  geo2lim  12333  mertenslem1  12342  mertens  12344  efcllem  12361  ef0lem  12362  efgt0  12385  eftlub  12391  eflt  12399  sinbnd  12462  cosbnd  12463  ef01bndlem  12466  sin01gt0  12472  cos01gt0  12473  sin02gt0  12474  eirrlem  12484  rpnnen2lem11  12505  rpnnen2  12506  ruclem11  12520  dvdssub2  12568  dvdsadd2b  12573  dvdsexp  12586  3dvds  12593  bitsfzolem  12627  bitscmp  12631  bitsinv1lem  12634  bezoutlem4  12722  dvdsgcd  12724  dvdsmulgcd  12735  nn0seqcvgd  12742  prmind2  12771  rpmulgcd2  12786  qredeq  12787  rpdvds  12805  divdenle  12822  hashdvds  12845  phimullem  12849  eulerthlem2  12852  prmdiveq  12856  prmdivdiv  12857  opoe  12866  pythagtriplem4  12874  pythagtriplem10  12875  pythagtriplem19  12888  iserodd  12890  pcpre1  12897  pcadd2  12940  qexpz  12951  expnprm  12952  pockthlem  12954  prmreclem2  12966  prmreclem3  12967  4sqlem7  12993  4sqlem10  12996  4sqlem11  13004  4sqlem12  13005  4sqlem14  13007  4sqlem15  13008  4sqlem16  13009  0ram  13069  ffthiso  13805  latmlej12  14199  divsgrp  14674  pgpfi1  14908  sylow1lem4  14914  sylow1lem5  14915  odcau  14917  pgpfi  14918  pgpssslw  14927  sylow3lem4  14943  sylow3lem6  14945  efgsfo  15050  frgp0  15071  odadd1  15142  odadd2  15143  odadd  15144  gexexlem  15146  lt6abl  15183  dprd2dlem1  15278  dprd2d2  15281  ablfacrplem  15302  ablfacrp  15303  ablfacrp2  15304  ablfac1b  15307  ablfac1eu  15310  pgpfac1lem3a  15313  ablfaclem2  15323  dvdsrid  15435  dvdsrtr  15436  dvdsrneg  15438  unitmulcl  15448  unitgrp  15451  unitnegcl  15465  isdrng2  15524  subrguss  15562  subrgunit  15565  abvsubtri  15602  fidomndrnglem  16049  psrbaglesupp  16116  gzrngunit  16439  prmirredlem  16448  znidomb  16517  mettri2  17908  xmetsym  17914  xmettri  17917  prdsxmetlem  17934  xblss2  17960  blhalf  17962  xmsge0  18011  ngptgp  18154  nrginvrcnlem  18203  nmoeq0  18247  cnmet  18283  blcvx  18306  opnreen  18338  metdcnlem  18343  metdstri  18357  metdsle  18358  metnrmlem1  18365  metnrmlem3  18367  lebnumlem1  18461  pi1inv  18552  cphnmf  18633  ipge0  18636  ipcau2  18666  tchcphlem1  18667  minveclem2  18792  minveclem3  18795  ovolssnul  18848  ovolctb  18851  ovolunnul  18861  ovoliunlem1  18863  ovoliun2  18867  ovoliunnul  18868  ioombl1lem4  18920  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  uniioombl  18946  volcn  18963  vitalilem2  18966  vitalilem5  18969  itg1lea  19069  mbfi1fseqlem6  19077  mbfi1flimlem  19079  itg2eqa  19102  itg2splitlem  19105  itg2split  19106  itg2monolem1  19107  itg2cnlem2  19119  iblabsr  19186  iblmulc2  19187  dveflem  19328  dvef  19329  dvferm2lem  19335  dvlip  19342  c1liplem1  19345  dveq0  19349  dvlt0  19354  dvivthlem1  19357  lhop1  19363  dvfsumle  19370  dvfsumlem4  19378  dvfsumrlim3  19382  dvfsum2  19383  ftc1a  19386  ftc1lem4  19388  deg1add  19491  ply1divex  19524  ply1rem  19551  fta1glem2  19554  fta1blem  19556  ig1pdvds  19564  plyeq0lem  19594  dgrcolem2  19657  plydivlem4  19678  plyrem  19687  fta1lem  19689  aalioulem3  19716  aaliou2b  19723  aaliou3lem3  19726  aaliou3lem8  19727  ulmcn  19778  ulmdvlem1  19779  itgulm  19786  pserulm  19800  pserdvlem2  19806  abelthlem2  19810  abelthlem5  19813  abelthlem6  19814  abelthlem7  19816  abelthlem8  19817  abelthlem9  19818  sinq12gt0  19877  sinq34lt0t  19879  cosq14gt0  19880  cosq14ge0  19881  efif1olem3  19908  argimgt0  19968  argimlt0  19969  logneg2  19971  logcnlem3  19993  logcnlem4  19994  logtayllem  20008  logtayl2  20011  cxpsqrlem  20051  cxpsqr  20052  cxpaddlelem  20093  abscxpbnd  20095  loglesqr  20100  ang180lem2  20110  atanlogaddlem  20211  atanlogsublem  20213  atantan  20221  atans2  20229  atantayl  20235  leibpi  20240  log2tlbnd  20243  birthdaylem2  20249  birthdaylem3  20250  cxp2limlem  20272  jensenlem2  20284  jensen  20285  emcllem2  20292  emcllem4  20294  harmonicbnd4  20306  fsumharmonic  20307  wilthlem3  20310  basellem1  20320  basellem3  20322  basellem4  20323  fsumdvdsdiaglem  20425  dvdsppwf1o  20428  dvdsmulf1o  20436  chteq0  20450  chtub  20453  chpub  20461  logfacubnd  20462  logfaclbnd  20463  logexprlim  20466  perfectlem2  20471  dchrfi  20496  bclbnd  20521  bposlem1  20525  bposlem3  20527  bposlem4  20528  bposlem6  20530  lgslem1  20537  lgsqrlem2  20583  lgsqrlem4  20585  lgseisenlem2  20591  lgsquadlem1  20595  lgsquadlem2  20596  lgsquad2lem1  20599  2sqlem3  20607  2sqlem4  20608  2sqlem8  20613  2sqlem11  20616  chebbnd1lem2  20621  chebbnd1lem3  20622  chtppilimlem1  20624  chpchtlim  20630  vmadivsum  20633  vmadivsumb  20634  rpvmasumlem  20638  dchrisumlem2  20641  dchrmusum2  20645  dchrvmasumlem2  20649  dchrvmasumlem3  20650  dchrisum0flblem2  20660  dchrisum0fno1  20662  dchrisum0re  20664  dchrisum0lem1  20667  dchrisum0lem2a  20668  mudivsum  20681  mulogsumlem  20682  mulog2sumlem2  20686  vmalogdivsum2  20689  selberglem2  20697  selbergb  20700  selberg2b  20703  logdivbnd  20707  selberg3lem1  20708  selberg3lem2  20709  selberg4lem1  20711  pntrmax  20715  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem5  20732  pntrlog2bndlem6a  20733  pntrlog2bndlem6  20734  pntrlog2bnd  20735  pntpbnd1a  20736  pntpbnd1  20737  pntpbnd2  20738  pntibndlem1  20740  pntibndlem2  20742  pntlemb  20748  pntlemq  20752  pntlemr  20753  pntlemj  20754  pntlemk  20757  qabvle  20776  padicabvcxp  20783  ostth2lem2  20785  ostth2lem3  20786  ostth2lem4  20787  ostth3  20789  nvge0  21242  smcnlem  21272  nmoub3i  21353  nmoub2i  21354  nmlno0lem  21373  minvecolem2  21456  htthlem  21499  norm3dif2  21732  bcs2  21763  chscllem2  22219  eigposi  22418  nmopub2tALT  22491  nmfnleub2  22508  nmlnop0iALT  22577  riesz1  22647  cnlnadjlem2  22650  nmopcoadji  22683  leopsq  22711  leopmul  22716  leopnmid  22720  nmopleid  22721  opsqrlem6  22727  0leopj  22768  hstle1  22808  strlem3a  22834  mdslmd4i  22915  cvexchlem  22950  cdj1i  23015  sqsscirc1  23294  xrge0tsmsd  23384  esumle  23435  esumlef  23437  esumcst  23438  dya2ub  23577  dya2iocseg  23581  subfacval3  23722  sconpht2  23771  sconpi1  23772  rescon  23779  snmlff  23914  sinccvglem  24007  mulge0b  24088  colinearalglem4  24539  axpaschlem  24570  axcontlem7  24600  btwnouttr2  24647  ltflcei  24930  itg2addnclem  24933  itg2addnc  24935  cntrset  25613  msra3  25620  csbrn  26473  geomcau  26486  bfplem2  26558  rrncmslem  26567  rrnequiv  26570  irrapxlem1  26918  pell1qrgaplem  26969  pell1qrgap  26970  monotoddzzfi  27038  jm2.24nn  27057  congtr  27063  congmul  27065  congsub  27068  fzmaxdif  27079  acongeq  27081  bezoutr1  27084  jm2.20nn  27101  jm2.25  27103  mapfien2  27269  hbtlem4  27341  dgrsub2  27350  mpaaeu  27366  idomsubgmo  27525  dvconstbi  27562  mulltgt0  27704  fmul01  27721  fmul01lt1lem1  27725  fmul01lt1lem2  27726  climrec  27740  climexp  27742  climneg  27747  stoweidlem1  27761  stoweidlem11  27771  stoweidlem13  27773  stoweidlem24  27784  stoweidlem26  27786  stoweidlem34  27794  stoweidlem38  27798  stoweidlem42  27802  stoweidlem51  27811  stoweidlem59  27819  wallispilem5  27829  wallispi2lem1  27831  wallispi2  27833  stirlinglem1  27834  stirlinglem5  27838  stirlinglem6  27839  stirlinglem7  27840  stirlinglem10  27843  stirlinglem11  27844  stirlinglem12  27845  stirlinglem13  27846  stirlinglem15  27848  lsatcvatlem  29312  islshpcv  29316  atlatmstc  29582  cvlsupr7  29611  cvrval3  29675  cvrval5  29677  cvrexchlem  29681  atcvrj1  29693  cvrat3  29704  cvrat4  29705  atbtwn  29708  1cvratex  29735  hlatexch4  29743  3atlem1  29745  3atlem2  29746  atcvrlln2  29781  atcvrlln  29782  lplnllnneN  29818  llncvrlpln2  29819  4atlem3b  29860  lplncvrlvol2  29877  dalemswapyz  29918  dalemswapyzps  29952  dalem25  29960  dalem39  29973  dalem58  29992  dalem59  29993  lneq2at  30040  lncvrat  30044  dalawlem2  30134  dalawlem3  30135  dalawlem4  30136  dalawlem6  30138  dalawlem9  30141  dalawlem11  30143  dalawlem12  30144  lhpocnle  30278  lhpmcvr3  30287  lhpmcvr5N  30289  lhpmcvr6N  30290  4atexlemunv  30328  4atexlemc  30331  4atexlemex2  30333  lautm  30356  cdlemc2  30454  cdleme5  30502  cdleme11j  30529  cdleme16b  30541  cdlemednpq  30561  cdleme19e  30569  cdleme20i  30579  cdleme22a  30602  cdleme22cN  30604  cdleme22d  30605  cdleme22e  30606  cdleme22eALTN  30607  cdleme22f  30608  cdleme23c  30613  cdleme30a  30640  cdleme35a  30710  cdleme35b  30712  cdleme42h  30744  cdlemeg46rgv  30790  cdlemg8b  30890  cdlemg12e  30909  cdlemg13a  30913  cdlemg17pq  30934  cdlemg18c  30942  cdlemg19  30946  cdlemg21  30948  cdlemg31d  30962  cdlemg33a  30968  tendoid  31035  cdlemk4  31096  cdlemki  31103  cdlemk10  31105  cdlemksv2  31109  cdlemk12  31112  cdlemk14  31116  cdlemk15  31117  cdlemk1u  31121  cdlemk5u  31123  cdlemk12u  31134  cdlemk45  31209  cdlemk48  31212  dia2dimlem1  31327  dia2dimlem2  31328  dia2dimlem3  31329  cdlemm10N  31381  cdlemn2  31458  dihjustlem  31479  dihglbcpreN  31563  dihmeetlem3N  31568
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator