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

Theorem breqtrd 4441
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 4428 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 215 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   class class class wbr 4416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417
This theorem is referenced by:  breqtrrd  4443  syl5breq  4452  domunsn  7748  mapdom2  7769  phplem4  7780  mapfien2  7948  wemaplem2  8088  infdifsn  8188  cantnff  8205  infxpenlem  8470  pwcda1  8650  pwcdadom  8672  infmap2  8674  ssfin4  8766  canthp1lem1  9103  nqereq  9386  ltexnq  9426  ltbtwnnq  9429  add20  10154  mullt0  10161  ltm1  10473  recgt0  10477  prodgt0  10478  prodge0  10480  ltmul1a  10482  mulge0b  10503  recp1lt1  10532  recreclt  10533  ledivp1  10536  ledivp1i  10560  ltdivp1i  10561  ltaddrp2d  11401  mul2lt0bi  11431  xleadd1a  11568  xov1plusxeqvd  11807  fz01en  11856  fzonmapblen  11992  fladdz  12090  flhalf  12094  fldiv  12119  modsubdir  12190  fzen2  12214  serle  12300  ltexp2a  12356  leexp2a  12360  exple1  12364  expubnd  12365  bernneq  12430  expmulnbnd  12436  discr1  12440  discr  12441  faclbnd6  12516  hashfz  12632  hashfun  12642  seqcoll  12660  sqeqd  13278  sqrlem7  13361  sqrtge0  13370  sqrtneglem  13379  abslt  13426  absle  13427  abstri  13442  rlimge0  13694  reccn2  13709  climaddc2  13748  isercolllem1  13777  caucvgrlem  13785  caucvgrlemOLD  13786  summolem2a  13830  isumge0  13876  fsumle  13908  fsumlt  13909  o1fsum  13922  supcvg  13963  expcnv  13971  geolim  13975  geolim2  13976  georeclim  13977  geo2lim  13980  mertenslem1  13989  mertens  13991  prodmolem2a  14037  efcllem  14181  ef0lem  14182  efgt0  14206  eftlub  14212  eflt  14220  sinbnd  14283  cosbnd  14284  ef01bndlem  14287  sin01gt0  14293  cos01gt0  14294  sin02gt0  14295  eirrlem  14305  rpnnen2lem11  14326  rpnnen2  14327  ruclem11  14341  dvdssub2  14391  dvdsadd2b  14396  dvdsexp  14410  3dvds  14418  bitsfzolem  14456  bitsfzolemOLD  14457  bitsinv1lem  14464  bezoutlem4OLD  14555  bezoutlem4  14558  dvdsgcd  14560  dvdsmulgcd  14571  nn0seqcvgd  14578  prmind2  14684  rpmulgcd2  14711  qredeq  14712  rpdvds  14725  divdenle  14747  hashdvds  14772  phimullem  14776  eulerthlem2  14779  prmdiveq  14783  prmdivdiv  14784  opoe  14810  pythagtriplem4  14818  pythagtriplem10  14819  pythagtriplem19  14832  iserodd  14834  pcpre1  14841  pcadd2  14884  qexpz  14895  expnprm  14896  pockthlem  14898  prmreclem2  14910  prmreclem3  14911  4sqlem7  14937  4sqlem10  14940  4sqlem11  14948  4sqlem12  14949  4sqlem14OLD  14951  4sqlem15OLD  14952  4sqlem16OLD  14953  4sqlem14  14957  4sqlem15  14958  4sqlem16  14959  0ram  15027  ffthiso  15883  latmlej12  16386  qusgrp  16921  pgpfi1  17296  sylow1lem4  17302  sylow1lem5  17303  odcau  17305  pgpfi  17306  pgpssslw  17315  sylow3lem4  17331  sylow3lem6  17333  efgsfo  17438  frgp0  17459  odadd1  17535  odadd2  17536  odadd  17537  gexexlem  17539  lt6abl  17578  gsumzsubmcl  17600  pwsgsum  17660  dprd2dlem1  17723  dprd2d2  17726  ablfacrplem  17747  ablfacrp  17748  ablfacrp2  17749  ablfac1b  17752  ablfac1eu  17755  pgpfac1lem3a  17758  ablfaclem2  17768  dvdsrid  17928  dvdsrtr  17929  dvdsrneg  17931  unitmulcl  17941  unitgrp  17944  unitnegcl  17958  isdrng2  18034  subrguss  18072  subrgunit  18075  abvsubtri  18112  fidomndrnglem  18579  psrbaglesupp  18641  gzrngunit  19082  prmirredlem  19113  znidomb  19181  frlmgsum  19379  invrvald  19750  psmetsym  21375  psmettri  21376  mettri2  21405  xmetsym  21411  xmettri  21415  prdsxmetlem  21432  xblss2ps  21465  xblss2  21466  blhalf  21469  xmsge0  21527  ngptgp  21693  nrginvrcnlem  21742  nmoeq0  21806  cnmet  21841  blcvx  21865  opnreen  21898  metdcnlem  21903  metdstri  21917  metdsle  21918  metnrmlem1  21925  metnrmlem3  21927  metdstriOLD  21932  metdsleOLD  21933  metnrmlem1OLD  21940  metnrmlem3OLD  21942  lebnumlem1  22038  lebnumlem1OLD  22041  pi1inv  22132  cphnmf  22222  ipge0  22225  ipcau2  22257  tchcphlem1  22258  csbren  22402  minveclem2  22417  minveclem3  22420  minveclem2OLD  22429  minveclem3OLD  22432  ovolssnul  22489  ovolctb  22492  ovolunnul  22502  ovoliunlem1  22504  ovoliun2  22508  ovoliunnul  22509  ioombl1lem4  22563  uniioombllem3  22592  uniioombllem4  22593  uniioombllem5  22594  uniioombl  22596  volcn  22613  vitalilem2  22616  vitalilem5  22619  itg1lea  22719  mbfi1fseqlem6  22727  mbfi1flimlem  22729  itg2eqa  22752  itg2splitlem  22755  itg2split  22756  itg2monolem1  22757  itg2cnlem2  22769  iblabsr  22836  iblmulc2  22837  dveflem  22980  dvef  22981  dvferm2lem  22987  dvlip  22994  c1liplem1  22997  dveq0  23001  dvlt0  23006  dvivthlem1  23009  lhop1  23015  dvfsumle  23022  dvfsumlem4  23030  dvfsumrlim3  23034  dvfsum2  23035  ftc1a  23038  ftc1lem4  23040  deg1add  23101  ply1divex  23136  ply1rem  23163  fta1glem2  23166  fta1blem  23168  ig1pdvds  23177  ig1pdvdsOLD  23183  plyeq0lem  23213  dgrcolem2  23277  plydivlem4  23298  plyrem  23307  fta1lem  23309  aalioulem3  23339  aaliou2b  23346  aaliou3lem3  23349  aaliou3lem8  23350  ulmcn  23403  ulmdvlem1  23404  itgulm  23412  pserulm  23426  pserdvlem2  23432  abelthlem2  23436  abelthlem5  23439  abelthlem6  23440  abelthlem7  23442  abelthlem8  23443  abelthlem9  23444  sinq12gt0  23511  sinq34lt0t  23513  cosq14gt0  23514  cosq14ge0  23515  efif1olem3  23542  argimgt0  23610  argimlt0  23611  logneg2  23613  logcnlem3  23638  logcnlem4  23639  logtayllem  23653  logtayl2  23656  cxpsqrtlem  23696  cxpsqrt  23697  cxpaddlelem  23740  abscxpbnd  23742  loglesqrt  23747  ang180lem2  23788  atanlogaddlem  23888  atanlogsublem  23890  atantan  23898  atans2  23906  atantayl  23912  leibpi  23917  log2tlbnd  23920  birthdaylem2  23927  birthdaylem3  23928  cxp2limlem  23950  jensenlem2  23962  jensen  23963  logdiflbnd  23969  emcllem2  23971  emcllem4  23973  harmonicbnd4  23985  fsumharmonic  23986  lgamgulmlem2  24004  lgamgulm2  24010  lgambdd  24011  lgamucov  24012  lgamcvglem  24014  lgamcvg2  24029  gamcvg  24030  wilthlem3  24044  basellem1  24056  basellem3  24058  basellem4  24059  fsumdvdsdiaglem  24161  dvdsppwf1o  24164  dvdsmulf1o  24172  chteq0  24186  chtub  24189  chpub  24197  logfacubnd  24198  logfaclbnd  24199  logexprlim  24202  perfectlem2  24207  dchrfi  24232  bclbnd  24257  bposlem1  24261  bposlem3  24263  bposlem4  24264  bposlem6  24266  lgslem1  24273  lgsqrlem2  24319  lgsqrlem4  24321  lgseisenlem2  24327  lgsquadlem1  24331  lgsquadlem2  24332  lgsquad2lem1  24335  2sqlem3  24343  2sqlem4  24344  2sqlem8  24349  2sqlem11  24352  chebbnd1lem2  24357  chebbnd1lem3  24358  chtppilimlem1  24360  chpchtlim  24366  vmadivsum  24369  vmadivsumb  24370  rpvmasumlem  24374  dchrisumlem2  24377  dchrmusum2  24381  dchrvmasumlem2  24385  dchrvmasumlem3  24386  dchrisum0flblem2  24396  dchrisum0fno1  24398  dchrisum0re  24400  dchrisum0lem1  24403  dchrisum0lem2a  24404  mudivsum  24417  mulogsumlem  24418  mulog2sumlem2  24422  vmalogdivsum2  24425  selberglem2  24433  selbergb  24436  selberg2b  24439  logdivbnd  24443  selberg3lem1  24444  selberg3lem2  24445  selberg4lem1  24447  pntrmax  24451  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem5  24468  pntrlog2bndlem6a  24469  pntrlog2bndlem6  24470  pntrlog2bnd  24471  pntpbnd1a  24472  pntpbnd1  24473  pntpbnd2  24474  pntibndlem1  24476  pntibndlem2  24478  pntlemb  24484  pntlemq  24488  pntlemr  24489  pntlemj  24490  pntlemk  24493  qabvle  24512  padicabvcxp  24519  ostth2lem2  24521  ostth2lem3  24522  ostth2lem4  24523  ostth3  24525  legtrid  24685  legov3  24692  krippenlem  24784  mideulem2  24825  midex  24828  opphllem5  24842  opphllem6  24843  opphl  24845  lmieu  24875  lmiisolem  24887  ttgcontlem1  24964  colinearalglem4  24988  axpaschlem  25019  axcontlem7  25049  clwlkndivn  25630  nvge0  26352  smcnlem  26382  nmoub3i  26463  nmoub2i  26464  nmlno0lem  26483  minvecolem2  26566  minvecolem2OLD  26576  htthlem  26619  norm3dif2  26853  bcs2  26884  chscllem2  27340  eigposi  27538  nmopub2tALT  27611  nmfnleub2  27628  nmlnop0iALT  27697  riesz1  27767  cnlnadjlem2  27770  nmopcoadji  27803  leopsq  27831  leopmul  27836  leopnmid  27840  nmopleid  27841  opsqrlem6  27847  0leopj  27888  hstle1  27928  strlem3a  27954  mdslmd4i  28035  cvexchlem  28070  cdj1i  28135  le2halvesd  28384  xlt2addrd  28387  2sqcoprm  28457  2sqmod  28458  archiabllem1a  28557  archiabllem2a  28560  archiabllem2c  28561  xrge0tsmsd  28597  orngsqr  28616  ornglmulle  28617  orngrmulle  28618  orng0le1  28624  fzto1st1  28664  metideq  28745  metider  28746  sqsscirc1  28763  esummono  28924  esumpad2  28926  esumle  28928  esumlef  28932  esumcst  28933  esumrnmpt2  28938  esum2d  28963  aean  29116  dya2ub  29141  dya2icoseg  29148  omssubadd  29177  omssubaddlemOLD  29180  omssubaddOLD  29181  inelcarsg  29192  carsgsigalem  29196  carsggect  29199  carsgclctunlem2  29200  eulerpartlemb  29250  fibp1  29283  sgnmulsgp  29470  eluzmn  29472  signsplypnf  29488  signsply0  29489  subfacval3  29961  sconpht2  30010  sconpi1  30011  rescon  30018  snmlff  30101  sinccvglem  30365  faclimlem2  30429  btwnouttr2  30838  ltflcei  31978  poimirlem9  31994  poimirlem26  32011  poimirlem27  32012  poimirlem29  32014  heicant  32020  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  volsupnfl  32030  dvtanlemOLD  32036  itg2addnclem  32038  itg2addnclem3  32040  iblmulc2nc  32052  bddiblnc  32057  ftc1cnnclem  32060  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  ftc2nc  32071  dvasin  32073  geomcau  32133  bfplem2  32200  rrncmslem  32209  rrnequiv  32212  lsatcvatlem  32660  islshpcv  32664  atlatmstc  32930  cvlsupr7  32959  cvrval3  33023  cvrval5  33025  cvrexchlem  33029  atcvrj1  33041  cvrat3  33052  cvrat4  33053  atbtwn  33056  1cvratex  33083  hlatexch4  33091  3atlem1  33093  3atlem2  33094  atcvrlln2  33129  atcvrlln  33130  lplnllnneN  33166  llncvrlpln2  33167  4atlem3b  33208  lplncvrlvol2  33225  dalemswapyz  33266  dalemswapyzps  33300  dalem25  33308  dalem39  33321  dalem58  33340  dalem59  33341  lneq2at  33388  lncvrat  33392  dalawlem2  33482  dalawlem3  33483  dalawlem4  33484  dalawlem6  33486  dalawlem9  33489  dalawlem11  33491  dalawlem12  33492  lhpocnle  33626  lhpmcvr3  33635  lhpmcvr5N  33637  lhpmcvr6N  33638  4atexlemunv  33676  4atexlemc  33679  4atexlemex2  33681  lautm  33704  cdlemc2  33803  cdleme5  33851  cdleme11j  33878  cdleme16b  33890  cdlemednpq  33910  cdleme19e  33919  cdleme20i  33929  cdleme22a  33952  cdleme22cN  33954  cdleme22d  33955  cdleme22e  33956  cdleme22eALTN  33957  cdleme22f  33958  cdleme23c  33963  cdleme30a  33990  cdleme35a  34060  cdleme35b  34062  cdleme42h  34094  cdlemeg46rgv  34140  cdlemg8b  34240  cdlemg12e  34259  cdlemg13a  34263  cdlemg17pq  34284  cdlemg18c  34292  cdlemg19  34296  cdlemg21  34298  cdlemg31d  34312  cdlemg33a  34318  tendoid  34385  cdlemk4  34446  cdlemki  34453  cdlemk10  34455  cdlemksv2  34459  cdlemk12  34462  cdlemk14  34466  cdlemk15  34467  cdlemk1u  34471  cdlemk5u  34473  cdlemk12u  34484  cdlemk45  34559  cdlemk48  34562  dia2dimlem1  34677  dia2dimlem2  34678  dia2dimlem3  34679  cdlemm10N  34731  cdlemn2  34808  dihjustlem  34829  dihglbcpreN  34913  dihmeetlem3N  34918  irrapxlem1  35711  pell1qrgaplem  35764  pell1qrgap  35765  monotoddzzfi  35835  jm2.24nn  35854  congtr  35860  congmul  35862  congsub  35865  fzmaxdif  35876  acongeq  35878  bezoutr1  35881  jm2.20nn  35897  jm2.25  35899  hbtlem4  36030  dgrsub2  36039  mpaaeu  36061  idomsubgmo  36117  int-sqgeq0d  36677  int-ineqmvtd  36682  cvgdvgrat  36706  radcnvrat  36707  hashnzfzclim  36715  dvconstbi  36727  binomcxplemdvbinom  36746  isosctrlem1ALT  37371  mulltgt0  37383  oddfl  37525  2timesgt  37539  lt3addmuld  37557  lt4addmuld  37562  supxrgere  37594  supxrgelem  37598  supxrge  37599  xadd0ge2  37602  infrpge  37612  xrlexaddrp  37613  xralrple2  37615  iccshift  37657  iooshift  37661  fsumnncl  37688  fmul01  37696  fmul01lt1lem1  37700  fmul01lt1lem2  37701  mccllem  37715  climrec  37719  climexp  37721  climneg  37727  limcrecl  37747  sumnnodd  37748  lptioo2  37749  lptioo1  37750  ltmod  37756  lptre2pt  37758  0ellimcdiv  37768  limclner  37770  cncficcgt0  37804  cncfioobdlem  37812  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem1OLD  37843  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dvdsn1add  37852  dvnxpaek  37855  dvnmul  37856  dvnprodlem1  37859  itgiccshift  37895  itgperiod  37896  stoweidlem1  37899  stoweidlem11  37909  stoweidlem13  37911  stoweidlem26  37924  stoweidlem34  37933  stoweidlem38  37937  stoweidlem42  37941  stoweidlem51  37950  stoweidlem59  37958  stirlinglem5  37978  stirlinglem6  37979  stirlinglem7  37980  stirlinglem10  37983  stirlinglem11  37984  stirlinglem13  37986  stirlinglem15  37988  dirkercncflem1  38003  dirkercncflem4  38006  fourierdlem4  38011  fourierdlem10  38017  fourierdlem11  38018  fourierdlem15  38022  fourierdlem20  38027  fourierdlem25  38032  fourierdlem26  38033  fourierdlem30  38037  fourierdlem37  38045  fourierdlem39  38047  fourierdlem40  38048  fourierdlem41  38049  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem44  38053  fourierdlem47  38055  fourierdlem48  38056  fourierdlem49  38057  fourierdlem50  38058  fourierdlem51  38059  fourierdlem52  38060  fourierdlem54  38062  fourierdlem60  38068  fourierdlem61  38069  fourierdlem63  38071  fourierdlem64  38072  fourierdlem65  38073  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem78  38086  fourierdlem79  38087  fourierdlem81  38089  fourierdlem84  38092  fourierdlem87  38095  fourierdlem92  38100  fourierdlem93  38101  fourierdlem101  38109  fourierdlem102  38110  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  fourierdlem114  38122  sqwvfoura  38130  sqwvfourb  38131  fouriersw  38133  etransclem19  38156  etransclem23  38160  etransclem24  38161  etransclem25  38162  etransclem27  38164  etransclem32  38169  etransclem35  38172  etransclem48OLD  38185  etransclem48  38186  qndenserrnbllem  38201  fsumlesge0  38257  sge0cl  38261  sge0supre  38269  sge0less  38272  sge0gerp  38275  sge0ltfirp  38280  sge0le  38287  sge0ltfirpmpt  38288  sge0split  38289  sge0rpcpnf  38301  sge0ltfirpmpt2  38306  sge0isum  38307  sge0xaddlem1  38313  sge0pnffigtmpt  38320  sge0pnffsumgt  38322  sge0gtfsumgt  38323  nnfoctbdjlem  38331  meassle  38339  omeiunle  38376  omeiunltfirp  38378  carageniuncllem2  38381  carageniuncl  38382  omess0  38393  hoicvr  38408  ovnlerp  38422  ovnsubaddlem1  38430  hsphoidmvle2  38445  hoidmv1lelem2  38452  hoidmv1le  38454  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvlelem5  38459  ovnhoilem2  38462  ovnhoi  38463  hoidifhspdmvle  38480  hoiqssbllem2  38483  hspmbllem2  38487  hspmbllem3  38488  hspmbl  38489  perfectALTVlem2  38882  nbfusgrlevtxm2  39502  nnpw2blen  40664
  Copyright terms: Public domain W3C validator