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

Theorem breqtrd 4238
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 4226 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 203 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   class class class wbr 4214
This theorem is referenced by:  breqtrrd  4240  syl5breq  4249  domunsn  7259  mapdom2  7280  phplem4  7291  wemaplem2  7518  infdifsn  7613  cantnff  7631  infxpenlem  7897  pwcda1  8076  pwcdadom  8098  infmap2  8100  ssfin4  8192  canthp1lem1  8529  nqereq  8814  ltexnq  8854  ltbtwnnq  8857  add20  9542  mullt0  9549  ltm1  9852  recgt0  9856  prodgt0  9857  prodge0  9859  ltmul1a  9861  recp1lt1  9910  recreclt  9911  ledivp1  9914  ledivp1i  9938  ltdivp1i  9939  ltaddrp2d  10680  xleadd1a  10834  xov1plusxeqvd  11043  fz01en  11081  fladdz  11229  flhalf  11233  fldiv  11243  modsubdir  11287  fzen2  11310  serle  11380  ltexp2a  11433  leexp2a  11437  exple1  11441  expubnd  11442  bernneq  11507  expmulnbnd  11513  discr1  11517  discr  11518  faclbnd6  11592  hashfz  11694  hashfun  11702  seqcoll  11714  sqeqd  11973  sqrlem7  12056  sqrge0  12065  sqrneglem  12074  abslt  12120  absle  12121  abstri  12136  rlimge0  12377  reccn2  12392  climaddc2  12431  isercolllem1  12460  caucvgrlem  12468  summolem2a  12511  isumge0  12552  fsumle  12580  fsumlt  12581  o1fsum  12594  supcvg  12637  expcnv  12645  geolim  12649  geolim2  12650  georeclim  12651  geo2lim  12654  mertenslem1  12663  mertens  12665  efcllem  12682  ef0lem  12683  efgt0  12706  eftlub  12712  eflt  12720  sinbnd  12783  cosbnd  12784  ef01bndlem  12787  sin01gt0  12793  cos01gt0  12794  sin02gt0  12795  eirrlem  12805  rpnnen2lem11  12826  rpnnen2  12827  ruclem11  12841  dvdssub2  12889  dvdsadd2b  12894  dvdsexp  12907  3dvds  12914  bitsfzolem  12948  bitsinv1lem  12955  bezoutlem4  13043  dvdsgcd  13045  dvdsmulgcd  13056  nn0seqcvgd  13063  prmind2  13092  rpmulgcd2  13107  qredeq  13108  rpdvds  13126  divdenle  13143  hashdvds  13166  phimullem  13170  eulerthlem2  13173  prmdiveq  13177  prmdivdiv  13178  opoe  13187  pythagtriplem4  13195  pythagtriplem10  13196  pythagtriplem19  13209  iserodd  13211  pcpre1  13218  pcadd2  13261  qexpz  13272  expnprm  13273  pockthlem  13275  prmreclem2  13287  prmreclem3  13288  4sqlem7  13314  4sqlem10  13317  4sqlem11  13325  4sqlem12  13326  4sqlem14  13328  4sqlem15  13329  4sqlem16  13330  0ram  13390  ffthiso  14128  latmlej12  14522  divsgrp  14997  pgpfi1  15231  sylow1lem4  15237  sylow1lem5  15238  odcau  15240  pgpfi  15241  pgpssslw  15250  sylow3lem4  15266  sylow3lem6  15268  efgsfo  15373  frgp0  15394  odadd1  15465  odadd2  15466  odadd  15467  gexexlem  15469  lt6abl  15506  dprd2dlem1  15601  dprd2d2  15604  ablfacrplem  15625  ablfacrp  15626  ablfacrp2  15627  ablfac1b  15630  ablfac1eu  15633  pgpfac1lem3a  15636  ablfaclem2  15646  dvdsrid  15758  dvdsrtr  15759  dvdsrneg  15761  unitmulcl  15771  unitgrp  15774  unitnegcl  15788  isdrng2  15847  subrguss  15885  subrgunit  15888  abvsubtri  15925  fidomndrnglem  16368  psrbaglesupp  16435  gzrngunit  16766  prmirredlem  16775  znidomb  16844  psmetsym  18343  psmettri  18344  mettri2  18373  xmetsym  18379  xmettri  18383  prdsxmetlem  18400  xblss2ps  18433  xblss2  18434  blhalf  18437  xmsge0  18495  ngptgp  18679  nrginvrcnlem  18728  nmoeq0  18772  cnmet  18808  blcvx  18831  opnreen  18864  metdcnlem  18869  metdstri  18883  metdsle  18884  metnrmlem1  18891  metnrmlem3  18893  lebnumlem1  18988  pi1inv  19079  cphnmf  19160  ipge0  19163  ipcau2  19193  tchcphlem1  19194  minveclem2  19329  minveclem3  19332  ovolssnul  19385  ovolctb  19388  ovolunnul  19398  ovoliunlem1  19400  ovoliun2  19404  ovoliunnul  19405  ioombl1lem4  19457  uniioombllem3  19479  uniioombllem4  19480  uniioombllem5  19481  uniioombl  19483  volcn  19500  vitalilem2  19503  vitalilem5  19506  itg1lea  19606  mbfi1fseqlem6  19614  mbfi1flimlem  19616  itg2eqa  19639  itg2splitlem  19642  itg2split  19643  itg2monolem1  19644  itg2cnlem2  19656  iblabsr  19723  iblmulc2  19724  dveflem  19865  dvef  19866  dvferm2lem  19872  dvlip  19879  c1liplem1  19882  dveq0  19886  dvlt0  19891  dvivthlem1  19894  lhop1  19900  dvfsumle  19907  dvfsumlem4  19915  dvfsumrlim3  19919  dvfsum2  19920  ftc1a  19923  ftc1lem4  19925  deg1add  20028  ply1divex  20061  ply1rem  20088  fta1glem2  20091  fta1blem  20093  ig1pdvds  20101  plyeq0lem  20131  dgrcolem2  20194  plydivlem4  20215  plyrem  20224  fta1lem  20226  aalioulem3  20253  aaliou2b  20260  aaliou3lem3  20263  aaliou3lem8  20264  ulmcn  20317  ulmdvlem1  20318  itgulm  20326  pserulm  20340  pserdvlem2  20346  abelthlem2  20350  abelthlem5  20353  abelthlem6  20354  abelthlem7  20356  abelthlem8  20357  abelthlem9  20358  sinq12gt0  20417  sinq34lt0t  20419  cosq14gt0  20420  cosq14ge0  20421  efif1olem3  20448  argimgt0  20509  argimlt0  20510  logneg2  20512  logcnlem3  20537  logcnlem4  20538  logtayllem  20552  logtayl2  20555  cxpsqrlem  20595  cxpsqr  20596  cxpaddlelem  20637  abscxpbnd  20639  loglesqr  20644  ang180lem2  20654  atanlogaddlem  20755  atanlogsublem  20757  atantan  20765  atans2  20773  atantayl  20779  leibpi  20784  log2tlbnd  20787  birthdaylem2  20793  birthdaylem3  20794  cxp2limlem  20816  jensenlem2  20828  jensen  20829  logdiflbnd  20835  emcllem2  20837  emcllem4  20839  harmonicbnd4  20851  fsumharmonic  20852  wilthlem3  20855  basellem1  20865  basellem3  20867  basellem4  20868  fsumdvdsdiaglem  20970  dvdsppwf1o  20973  dvdsmulf1o  20981  chteq0  20995  chtub  20998  chpub  21006  logfacubnd  21007  logfaclbnd  21008  logexprlim  21011  perfectlem2  21016  dchrfi  21041  bclbnd  21066  bposlem1  21070  bposlem3  21072  bposlem4  21073  bposlem6  21075  lgslem1  21082  lgsqrlem2  21128  lgsqrlem4  21130  lgseisenlem2  21136  lgsquadlem1  21140  lgsquadlem2  21141  lgsquad2lem1  21144  2sqlem3  21152  2sqlem4  21153  2sqlem8  21158  2sqlem11  21161  chebbnd1lem2  21166  chebbnd1lem3  21167  chtppilimlem1  21169  chpchtlim  21175  vmadivsum  21178  vmadivsumb  21179  rpvmasumlem  21183  dchrisumlem2  21186  dchrmusum2  21190  dchrvmasumlem2  21194  dchrvmasumlem3  21195  dchrisum0flblem2  21205  dchrisum0fno1  21207  dchrisum0re  21209  dchrisum0lem1  21212  dchrisum0lem2a  21213  mudivsum  21226  mulogsumlem  21227  mulog2sumlem2  21231  vmalogdivsum2  21234  selberglem2  21242  selbergb  21245  selberg2b  21248  logdivbnd  21252  selberg3lem1  21253  selberg3lem2  21254  selberg4lem1  21256  pntrmax  21260  pntrlog2bndlem2  21274  pntrlog2bndlem3  21275  pntrlog2bndlem5  21277  pntrlog2bndlem6a  21278  pntrlog2bndlem6  21279  pntrlog2bnd  21280  pntpbnd1a  21281  pntpbnd1  21282  pntpbnd2  21283  pntibndlem1  21285  pntibndlem2  21287  pntlemb  21293  pntlemq  21297  pntlemr  21298  pntlemj  21299  pntlemk  21302  qabvle  21321  padicabvcxp  21328  ostth2lem2  21330  ostth2lem3  21331  ostth2lem4  21332  ostth3  21334  nvge0  22165  smcnlem  22195  nmoub3i  22276  nmoub2i  22277  nmlno0lem  22296  minvecolem2  22379  htthlem  22422  norm3dif2  22655  bcs2  22686  chscllem2  23142  eigposi  23341  nmopub2tALT  23414  nmfnleub2  23431  nmlnop0iALT  23500  riesz1  23570  cnlnadjlem2  23573  nmopcoadji  23606  leopsq  23634  leopmul  23639  leopnmid  23643  nmopleid  23644  opsqrlem6  23650  0leopj  23691  hstle1  23731  strlem3a  23757  mdslmd4i  23838  cvexchlem  23873  cdj1i  23938  le2halvesd  24124  xlt2addrd  24126  xrge0tsmsd  24225  ofldsqr  24242  ofld0le1  24244  metideq  24290  metider  24291  sqsscirc1  24308  esumle  24451  esummono  24452  esumlef  24456  esumcst  24457  aean  24597  dya2ub  24622  dya2icoseg  24629  lgamgulmlem2  24816  lgamgulm2  24822  lgambdd  24823  lgamucov  24824  lgamcvglem  24826  lgamcvg2  24841  gamcvg  24842  subfacval3  24877  sconpht2  24927  sconpi1  24928  rescon  24935  snmlff  25018  sinccvglem  25111  mulge0b  25193  prodmolem2a  25262  faclimlem2  25365  colinearalglem4  25850  axpaschlem  25881  axcontlem7  25911  btwnouttr2  25958  ltflcei  26241  mblfinlem2  26246  mblfinlem3  26247  mblfinlem4  26248  volsupnfl  26253  itg2addnclem  26258  itg2addnclem3  26260  iblmulc2nc  26272  bddiblnc  26277  ftc1cnnclem  26280  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc2nc  26291  csbrn  26458  geomcau  26467  bfplem2  26534  rrncmslem  26543  rrnequiv  26546  irrapxlem1  26887  pell1qrgaplem  26938  pell1qrgap  26939  monotoddzzfi  27007  jm2.24nn  27026  congtr  27032  congmul  27034  congsub  27037  fzmaxdif  27048  acongeq  27050  bezoutr1  27053  jm2.20nn  27070  jm2.25  27072  mapfien2  27237  hbtlem4  27309  dgrsub2  27318  mpaaeu  27334  idomsubgmo  27493  dvconstbi  27530  mulltgt0  27671  fmul01  27688  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climrec  27707  climexp  27709  climneg  27714  stoweidlem1  27728  stoweidlem11  27738  stoweidlem13  27740  stoweidlem26  27753  stoweidlem34  27761  stoweidlem38  27765  stoweidlem42  27769  stoweidlem51  27778  stoweidlem59  27786  stirlinglem5  27805  stirlinglem6  27806  stirlinglem7  27807  stirlinglem10  27810  stirlinglem11  27811  stirlinglem12  27812  stirlinglem13  27813  stirlinglem15  27815  fzonmapblen  28145  isosctrlem1ALT  29108  lsatcvatlem  29909  islshpcv  29913  atlatmstc  30179  cvlsupr7  30208  cvrval3  30272  cvrval5  30274  cvrexchlem  30278  atcvrj1  30290  cvrat3  30301  cvrat4  30302  atbtwn  30305  1cvratex  30332  hlatexch4  30340  3atlem1  30342  3atlem2  30343  atcvrlln2  30378  atcvrlln  30379  lplnllnneN  30415  llncvrlpln2  30416  4atlem3b  30457  lplncvrlvol2  30474  dalemswapyz  30515  dalemswapyzps  30549  dalem25  30557  dalem39  30570  dalem58  30589  dalem59  30590  lneq2at  30637  lncvrat  30641  dalawlem2  30731  dalawlem3  30732  dalawlem4  30733  dalawlem6  30735  dalawlem9  30738  dalawlem11  30740  dalawlem12  30741  lhpocnle  30875  lhpmcvr3  30884  lhpmcvr5N  30886  lhpmcvr6N  30887  4atexlemunv  30925  4atexlemc  30928  4atexlemex2  30930  lautm  30953  cdlemc2  31051  cdleme5  31099  cdleme11j  31126  cdleme16b  31138  cdlemednpq  31158  cdleme19e  31166  cdleme20i  31176  cdleme22a  31199  cdleme22cN  31201  cdleme22d  31202  cdleme22e  31203  cdleme22eALTN  31204  cdleme22f  31205  cdleme23c  31210  cdleme30a  31237  cdleme35a  31307  cdleme35b  31309  cdleme42h  31341  cdlemeg46rgv  31387  cdlemg8b  31487  cdlemg12e  31506  cdlemg13a  31510  cdlemg17pq  31531  cdlemg18c  31539  cdlemg19  31543  cdlemg21  31545  cdlemg31d  31559  cdlemg33a  31565  tendoid  31632  cdlemk4  31693  cdlemki  31700  cdlemk10  31702  cdlemksv2  31706  cdlemk12  31709  cdlemk14  31713  cdlemk15  31714  cdlemk1u  31718  cdlemk5u  31720  cdlemk12u  31731  cdlemk45  31806  cdlemk48  31809  dia2dimlem1  31924  dia2dimlem2  31925  dia2dimlem3  31926  cdlemm10N  31978  cdlemn2  32055  dihjustlem  32076  dihglbcpreN  32160  dihmeetlem3N  32165
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4215
  Copyright terms: Public domain W3C validator