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

Theorem breqtrd 4200
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 4188 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 202 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4176
This theorem is referenced by:  breqtrrd  4202  syl5breq  4211  domunsn  7220  mapdom2  7241  phplem4  7252  wemaplem2  7476  infdifsn  7571  cantnff  7589  infxpenlem  7855  pwcda1  8034  pwcdadom  8056  infmap2  8058  ssfin4  8150  canthp1lem1  8487  nqereq  8772  ltexnq  8812  ltbtwnnq  8815  add20  9500  mullt0  9507  ltm1  9810  recgt0  9814  prodgt0  9815  prodge0  9817  ltmul1a  9819  recp1lt1  9868  recreclt  9869  ledivp1  9872  ledivp1i  9896  ltdivp1i  9897  ltaddrp2d  10638  xleadd1a  10792  xov1plusxeqvd  11001  fz01en  11039  fladdz  11186  flhalf  11190  fldiv  11200  modsubdir  11244  fzen2  11267  serle  11337  ltexp2a  11390  leexp2a  11394  exple1  11398  expubnd  11399  bernneq  11464  expmulnbnd  11470  discr1  11474  discr  11475  faclbnd6  11549  hashfz  11651  hashfun  11659  seqcoll  11671  sqeqd  11930  sqrlem7  12013  sqrge0  12022  sqrneglem  12031  abslt  12077  absle  12078  abstri  12093  rlimge0  12334  reccn2  12349  climaddc2  12388  isercolllem1  12417  caucvgrlem  12425  summolem2a  12468  isumge0  12509  fsumle  12537  fsumlt  12538  o1fsum  12551  supcvg  12594  expcnv  12602  geolim  12606  geolim2  12607  georeclim  12608  geo2lim  12611  mertenslem1  12620  mertens  12622  efcllem  12639  ef0lem  12640  efgt0  12663  eftlub  12669  eflt  12677  sinbnd  12740  cosbnd  12741  ef01bndlem  12744  sin01gt0  12750  cos01gt0  12751  sin02gt0  12752  eirrlem  12762  rpnnen2lem11  12783  rpnnen2  12784  ruclem11  12798  dvdssub2  12846  dvdsadd2b  12851  dvdsexp  12864  3dvds  12871  bitsfzolem  12905  bitsinv1lem  12912  bezoutlem4  13000  dvdsgcd  13002  dvdsmulgcd  13013  nn0seqcvgd  13020  prmind2  13049  rpmulgcd2  13064  qredeq  13065  rpdvds  13083  divdenle  13100  hashdvds  13123  phimullem  13127  eulerthlem2  13130  prmdiveq  13134  prmdivdiv  13135  opoe  13144  pythagtriplem4  13152  pythagtriplem10  13153  pythagtriplem19  13166  iserodd  13168  pcpre1  13175  pcadd2  13218  qexpz  13229  expnprm  13230  pockthlem  13232  prmreclem2  13244  prmreclem3  13245  4sqlem7  13271  4sqlem10  13274  4sqlem11  13282  4sqlem12  13283  4sqlem14  13285  4sqlem15  13286  4sqlem16  13287  0ram  13347  ffthiso  14085  latmlej12  14479  divsgrp  14954  pgpfi1  15188  sylow1lem4  15194  sylow1lem5  15195  odcau  15197  pgpfi  15198  pgpssslw  15207  sylow3lem4  15223  sylow3lem6  15225  efgsfo  15330  frgp0  15351  odadd1  15422  odadd2  15423  odadd  15424  gexexlem  15426  lt6abl  15463  dprd2dlem1  15558  dprd2d2  15561  ablfacrplem  15582  ablfacrp  15583  ablfacrp2  15584  ablfac1b  15587  ablfac1eu  15590  pgpfac1lem3a  15593  ablfaclem2  15603  dvdsrid  15715  dvdsrtr  15716  dvdsrneg  15718  unitmulcl  15728  unitgrp  15731  unitnegcl  15745  isdrng2  15804  subrguss  15842  subrgunit  15845  abvsubtri  15882  fidomndrnglem  16325  psrbaglesupp  16392  gzrngunit  16723  prmirredlem  16732  znidomb  16801  psmetsym  18298  psmettri  18299  mettri2  18328  xmetsym  18334  xmettri  18338  prdsxmetlem  18355  xblss2ps  18388  xblss2  18389  blhalf  18392  xmsge0  18450  ngptgp  18634  nrginvrcnlem  18683  nmoeq0  18727  cnmet  18763  blcvx  18786  opnreen  18819  metdcnlem  18824  metdstri  18838  metdsle  18839  metnrmlem1  18846  metnrmlem3  18848  lebnumlem1  18943  pi1inv  19034  cphnmf  19115  ipge0  19118  ipcau2  19148  tchcphlem1  19149  minveclem2  19284  minveclem3  19287  ovolssnul  19340  ovolctb  19343  ovolunnul  19353  ovoliunlem1  19355  ovoliun2  19359  ovoliunnul  19360  ioombl1lem4  19412  uniioombllem3  19434  uniioombllem4  19435  uniioombllem5  19436  uniioombl  19438  volcn  19455  vitalilem2  19458  vitalilem5  19461  itg1lea  19561  mbfi1fseqlem6  19569  mbfi1flimlem  19571  itg2eqa  19594  itg2splitlem  19597  itg2split  19598  itg2monolem1  19599  itg2cnlem2  19611  iblabsr  19678  iblmulc2  19679  dveflem  19820  dvef  19821  dvferm2lem  19827  dvlip  19834  c1liplem1  19837  dveq0  19841  dvlt0  19846  dvivthlem1  19849  lhop1  19855  dvfsumle  19862  dvfsumlem4  19870  dvfsumrlim3  19874  dvfsum2  19875  ftc1a  19878  ftc1lem4  19880  deg1add  19983  ply1divex  20016  ply1rem  20043  fta1glem2  20046  fta1blem  20048  ig1pdvds  20056  plyeq0lem  20086  dgrcolem2  20149  plydivlem4  20170  plyrem  20179  fta1lem  20181  aalioulem3  20208  aaliou2b  20215  aaliou3lem3  20218  aaliou3lem8  20219  ulmcn  20272  ulmdvlem1  20273  itgulm  20281  pserulm  20295  pserdvlem2  20301  abelthlem2  20305  abelthlem5  20308  abelthlem6  20309  abelthlem7  20311  abelthlem8  20312  abelthlem9  20313  sinq12gt0  20372  sinq34lt0t  20374  cosq14gt0  20375  cosq14ge0  20376  efif1olem3  20403  argimgt0  20464  argimlt0  20465  logneg2  20467  logcnlem3  20492  logcnlem4  20493  logtayllem  20507  logtayl2  20510  cxpsqrlem  20550  cxpsqr  20551  cxpaddlelem  20592  abscxpbnd  20594  loglesqr  20599  ang180lem2  20609  atanlogaddlem  20710  atanlogsublem  20712  atantan  20720  atans2  20728  atantayl  20734  leibpi  20739  log2tlbnd  20742  birthdaylem2  20748  birthdaylem3  20749  cxp2limlem  20771  jensenlem2  20783  jensen  20784  logdiflbnd  20790  emcllem2  20792  emcllem4  20794  harmonicbnd4  20806  fsumharmonic  20807  wilthlem3  20810  basellem1  20820  basellem3  20822  basellem4  20823  fsumdvdsdiaglem  20925  dvdsppwf1o  20928  dvdsmulf1o  20936  chteq0  20950  chtub  20953  chpub  20961  logfacubnd  20962  logfaclbnd  20963  logexprlim  20966  perfectlem2  20971  dchrfi  20996  bclbnd  21021  bposlem1  21025  bposlem3  21027  bposlem4  21028  bposlem6  21030  lgslem1  21037  lgsqrlem2  21083  lgsqrlem4  21085  lgseisenlem2  21091  lgsquadlem1  21095  lgsquadlem2  21096  lgsquad2lem1  21099  2sqlem3  21107  2sqlem4  21108  2sqlem8  21113  2sqlem11  21116  chebbnd1lem2  21121  chebbnd1lem3  21122  chtppilimlem1  21124  chpchtlim  21130  vmadivsum  21133  vmadivsumb  21134  rpvmasumlem  21138  dchrisumlem2  21141  dchrmusum2  21145  dchrvmasumlem2  21149  dchrvmasumlem3  21150  dchrisum0flblem2  21160  dchrisum0fno1  21162  dchrisum0re  21164  dchrisum0lem1  21167  dchrisum0lem2a  21168  mudivsum  21181  mulogsumlem  21182  mulog2sumlem2  21186  vmalogdivsum2  21189  selberglem2  21197  selbergb  21200  selberg2b  21203  logdivbnd  21207  selberg3lem1  21208  selberg3lem2  21209  selberg4lem1  21211  pntrmax  21215  pntrlog2bndlem2  21229  pntrlog2bndlem3  21230  pntrlog2bndlem5  21232  pntrlog2bndlem6a  21233  pntrlog2bndlem6  21234  pntrlog2bnd  21235  pntpbnd1a  21236  pntpbnd1  21237  pntpbnd2  21238  pntibndlem1  21240  pntibndlem2  21242  pntlemb  21248  pntlemq  21252  pntlemr  21253  pntlemj  21254  pntlemk  21257  qabvle  21276  padicabvcxp  21283  ostth2lem2  21285  ostth2lem3  21286  ostth2lem4  21287  ostth3  21289  nvge0  22120  smcnlem  22150  nmoub3i  22231  nmoub2i  22232  nmlno0lem  22251  minvecolem2  22334  htthlem  22377  norm3dif2  22610  bcs2  22641  chscllem2  23097  eigposi  23296  nmopub2tALT  23369  nmfnleub2  23386  nmlnop0iALT  23455  riesz1  23525  cnlnadjlem2  23528  nmopcoadji  23561  leopsq  23589  leopmul  23594  leopnmid  23598  nmopleid  23599  opsqrlem6  23605  0leopj  23646  hstle1  23686  strlem3a  23712  mdslmd4i  23793  cvexchlem  23828  cdj1i  23893  le2halvesd  24079  xlt2addrd  24081  xrge0tsmsd  24180  ofldsqr  24197  ofld0le1  24199  metideq  24245  metider  24246  sqsscirc1  24263  esumle  24406  esummono  24407  esumlef  24411  esumcst  24412  aean  24552  dya2ub  24577  dya2icoseg  24584  lgamgulmlem2  24771  lgamgulm2  24777  lgambdd  24778  lgamucov  24779  lgamcvglem  24781  lgamcvg2  24796  gamcvg  24797  subfacval3  24832  sconpht2  24882  sconpi1  24883  rescon  24890  snmlff  24973  sinccvglem  25066  mulge0b  25148  prodmolem2a  25217  faclimlem2  25315  colinearalglem4  25756  axpaschlem  25787  axcontlem7  25817  btwnouttr2  25864  ltflcei  26144  mblfinlem  26147  mblfinlem2  26148  mblfinlem3  26149  volsupnfl  26154  itg2addnclem  26159  itg2addnclem3  26161  iblmulc2nc  26173  bddiblnc  26178  ftc1cnnclem  26181  csbrn  26350  geomcau  26359  bfplem2  26426  rrncmslem  26435  rrnequiv  26438  irrapxlem1  26779  pell1qrgaplem  26830  pell1qrgap  26831  monotoddzzfi  26899  jm2.24nn  26918  congtr  26924  congmul  26926  congsub  26929  fzmaxdif  26940  acongeq  26942  bezoutr1  26945  jm2.20nn  26962  jm2.25  26964  mapfien2  27130  hbtlem4  27202  dgrsub2  27211  mpaaeu  27227  idomsubgmo  27386  dvconstbi  27423  mulltgt0  27564  fmul01  27581  fmul01lt1lem1  27585  fmul01lt1lem2  27586  climrec  27600  climexp  27602  climneg  27607  stoweidlem1  27621  stoweidlem11  27631  stoweidlem13  27633  stoweidlem26  27646  stoweidlem34  27654  stoweidlem38  27658  stoweidlem42  27662  stoweidlem51  27671  stoweidlem59  27679  stirlinglem5  27698  stirlinglem6  27699  stirlinglem7  27700  stirlinglem10  27703  stirlinglem11  27704  stirlinglem12  27705  stirlinglem13  27706  stirlinglem15  27708  lsatcvatlem  29536  islshpcv  29540  atlatmstc  29806  cvlsupr7  29835  cvrval3  29899  cvrval5  29901  cvrexchlem  29905  atcvrj1  29917  cvrat3  29928  cvrat4  29929  atbtwn  29932  1cvratex  29959  hlatexch4  29967  3atlem1  29969  3atlem2  29970  atcvrlln2  30005  atcvrlln  30006  lplnllnneN  30042  llncvrlpln2  30043  4atlem3b  30084  lplncvrlvol2  30101  dalemswapyz  30142  dalemswapyzps  30176  dalem25  30184  dalem39  30197  dalem58  30216  dalem59  30217  lneq2at  30264  lncvrat  30268  dalawlem2  30358  dalawlem3  30359  dalawlem4  30360  dalawlem6  30362  dalawlem9  30365  dalawlem11  30367  dalawlem12  30368  lhpocnle  30502  lhpmcvr3  30511  lhpmcvr5N  30513  lhpmcvr6N  30514  4atexlemunv  30552  4atexlemc  30555  4atexlemex2  30557  lautm  30580  cdlemc2  30678  cdleme5  30726  cdleme11j  30753  cdleme16b  30765  cdlemednpq  30785  cdleme19e  30793  cdleme20i  30803  cdleme22a  30826  cdleme22cN  30828  cdleme22d  30829  cdleme22e  30830  cdleme22eALTN  30831  cdleme22f  30832  cdleme23c  30837  cdleme30a  30864  cdleme35a  30934  cdleme35b  30936  cdleme42h  30968  cdlemeg46rgv  31014  cdlemg8b  31114  cdlemg12e  31133  cdlemg13a  31137  cdlemg17pq  31158  cdlemg18c  31166  cdlemg19  31170  cdlemg21  31172  cdlemg31d  31186  cdlemg33a  31192  tendoid  31259  cdlemk4  31320  cdlemki  31327  cdlemk10  31329  cdlemksv2  31333  cdlemk12  31336  cdlemk14  31340  cdlemk15  31341  cdlemk1u  31345  cdlemk5u  31347  cdlemk12u  31358  cdlemk45  31433  cdlemk48  31436  dia2dimlem1  31551  dia2dimlem2  31552  dia2dimlem3  31553  cdlemm10N  31605  cdlemn2  31682  dihjustlem  31703  dihglbcpreN  31787  dihmeetlem3N  31792
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177
  Copyright terms: Public domain W3C validator