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

Theorem breqtrrd 4443
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1  |-  ( ph  ->  A R B )
breqtrrd.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
breqtrrd  |-  ( ph  ->  A R C )

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2428 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4441 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418
This theorem is referenced by:  marypha1lem  7944  marypha2  7950  unxpwdom  8095  uncdadom  8590  cdacomen  8600  cdaassen  8601  xpcdaen  8602  onacda  8616  infcdaabs  8625  cfss  8684  tskuni  9197  ltexnq  9389  mul2lt0rgt0  11388  xrmax1  11459  xrmax2  11460  max1ALT  11470  qbtwnxr  11482  xleadd1a  11528  xlt2add  11535  xlesubadd  11538  xmulgt0  11558  xlemul1a  11563  xov1plusxeqvd  11765  uzsubsubfz  11808  fzctr  11890  flflp1  12029  ceilge  12059  modge0  12092  modlt  12093  modid  12107  modaddmodup  12139  sermono  12231  seqf1olem1  12238  seqf1olem2  12239  leexp1a  12317  sqgt0  12329  sqge0  12337  nnlesq  12364  expnbnd  12387  expmulnbnd  12390  discr1  12394  facwordi  12460  faclbnd5  12469  hashdom  12544  brfi1uzind  12630  ccatws1n0  12739  swrds2  12988  cjmulge0  13177  resqrtcl  13285  absge0  13318  sqreulem  13390  amgm2  13400  rlimdm  13582  rlimge0  13612  reccn2  13627  climle  13670  climserle  13693  isercoll2  13699  iseraltlem1  13715  iseralt  13718  isumclim2  13786  isumclim3  13787  isumge0  13794  fsumless  13823  cvgcmp  13843  cvgcmpce  13845  abscvgcvg  13846  isumsup2  13871  isumltss  13873  climcndslem1  13874  climcnds  13876  supcvg  13881  harmonic  13884  expcnv  13889  explecnv  13890  cvgrat  13906  mertenslem1  13907  mertenslem2  13908  clim2div  13912  ntrivcvgtail  13923  iprodclim2  14019  iprodclim3  14020  efcvg  14106  ege2le3  14111  efaddlem  14114  eftlub  14130  effsumlt  14132  tanhlt1  14181  ef01bndlem  14205  sin02gt0  14213  rpnnen2lem4  14237  ruclem2  14251  ruclem3  14252  ruclem9  14257  iddvdsexp  14293  dvdsadd  14310  dvdsfac  14327  dvdsmod  14329  3dvds  14336  divalglem1  14339  bitsfzo  14372  bitsmod  14373  bitscmp  14375  bitsinv1lem  14378  sadcaddlem  14394  sadadd3  14398  sadaddlem  14403  dvdssqim  14481  dvdsmulgcd  14482  nn0seqcvgd  14489  dvdslcm  14523  lcmgcdlem  14531  dvdslcmf  14564  lcmfunsnlem2lem2  14572  sqnprm  14606  mulgcddvds  14621  qredeq  14623  isprm6  14626  nonsq  14668  hashdvds  14681  prmdiv  14691  odzdvds  14698  omoe  14714  pythagtriplem4  14721  pcpre1  14744  pcdvdsb  14770  pcz  14782  pcprmpw2  14783  pcaddlem  14785  pcadd  14786  pcadd2  14787  pcmpt  14789  pcmptdvds  14791  fldivp1  14794  pcfaclem  14795  pockthlem  14801  prmreclem1  14812  prmreclem3  14814  prmreclem5  14816  prmreclem6  14817  4sqlem6  14839  4sqlem8  14841  4sqlem11  14851  4sqlem12  14852  4sqlem14OLD  14854  4sqlem16OLD  14856  4sqlem14  14860  4sqlem16  14862  vdwlem3  14885  vdwlem9  14891  vdwlem10  14892  vdwlem12  14894  ramub1lem2  14937  prmorlefacOLD  14970  prmgap  14981  prmgaplcmOLD  14982  prmgaplcm  14983  prmgapprmo  14985  invfuc  15823  ple1  16234  eqgen  16814  lagsubg  16823  pgpfi  17185  sylow2alem2  17198  sylow2a  17199  sylow3lem4  17210  efgsrel  17312  odadd1  17414  odadd2  17415  gexex  17419  lt6abl  17457  dprd2d2  17605  dmdprdpr  17610  ablfacrp2  17628  ablfac1c  17632  pgpfaclem1  17642  ablfac2  17650  dvdsrmul1  17809  unitmulclb  17821  subrguss  17951  abvres  17995  ply1coefsupp  18816  evl1gsumadd  18874  znfld  19055  znunit  19058  frlmisfrlm  19330  matgsum  19386  pm2mpcl  19745  psmetxrge0  21253  isxmet2d  21266  mettri  21291  xmettri3  21292  mettri3  21293  xmetrtri2  21295  prdsxmetlem  21307  imasdsf1olem  21312  xblss2ps  21340  blss2ps  21342  blss2  21343  blssps  21363  blss  21364  prdsbl  21430  dscmet  21511  nmge0  21554  nmmtri  21559  nlmvscnlem2  21612  nrginvrcnlem  21617  nmoix  21654  nmoleub  21656  blcvx  21720  xrsxmet  21731  opnreen  21753  xrge0tsms  21756  icopnfcnv  21859  xrhmeo  21863  lebnumii  21883  pcophtb  21946  pi1grplem  21966  nmoleub2lem  22014  ipcau2  22094  tchcphlem1  22095  ipcau  22098  ipcnlem2  22101  rrxcph  22237  minveclem2  22254  minveclem3b  22256  pjthlem1  22265  pjthlem2  22266  ivthlem3  22278  ivth2  22280  ovolfsf  22298  ovolsslem  22311  ovollb2lem  22315  ovollb2  22316  ovolctb  22317  ovolfiniun  22328  ovolicc1  22343  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  ovolicc2  22350  nulmbl2  22364  unmbl  22365  ioombl1lem4  22388  uniioombllem4  22418  uniioombllem6  22420  volivth  22439  vitalilem4  22443  itg1ge0  22518  itg1ge0a  22543  itg1lea  22544  itg1climres  22546  mbfi1fseqlem5  22551  itg2ub  22565  itg2seq  22574  itg2uba  22575  itg2splitlem  22580  itg2split  22581  itg2monolem3  22584  itg2mono  22585  itg2i1fseq2  22588  itg2addlem  22590  iblss  22636  itggt0  22673  dvferm2lem  22812  dvlip  22819  dvivthlem1  22834  dvfsumlem2  22853  dvfsumlem3  22854  ftc1lem4  22865  ply1divmo  22958  ply1remlem  22985  fta1glem2  22989  ig1pdvds  22999  plyeq0lem  23029  plydiveu  23116  fta1lem  23125  vieta1lem2  23129  aaliou3lem2  23161  aaliou3lem8  23163  ulmcn  23216  mtest  23221  itgulm  23225  radcnvlem1  23230  radcnvlt1  23235  dvradcnv  23238  pserdvlem2  23245  abelthlem2  23249  abelthlem6  23253  abelthlem7  23255  abelthlem9  23257  tangtx  23322  sinq12gt0  23324  sineq0  23338  cosordlem  23342  tanord  23349  tanregt0  23350  logrnaddcl  23386  logcj  23417  argregt0  23421  argrege0  23422  argimgt0  23423  argimlt0  23424  logimul  23425  logneg2  23426  logdivlti  23431  divlogrlim  23442  logcnlem3  23451  logcnlem4  23452  dvlog2lem  23459  logtayl  23467  rpcxpcl  23483  cxpsqrtlem  23509  cxpaddle  23554  isosctrlem1  23609  asinlem3a  23658  asinlem3  23659  asinneg  23674  asinsinlem  23679  asinsin  23680  atanlogaddlem  23701  atanlogadd  23702  atanlogsublem  23703  atanlogsub  23704  atantan  23711  atanbndlem  23713  atantayl  23725  leibpi  23730  birthdaylem3  23741  areaf  23749  cxploglim  23765  jensenlem2  23775  jensen  23776  logdiflbnd  23782  harmonicbnd4  23798  fsumharmonic  23799  zetacvg  23802  lgamgulmlem2  23817  lgamgulmlem3  23818  lgamcvg2  23842  wilthlem2  23856  ftalem1  23859  ftalem2  23860  ftalem5  23863  basellem6  23872  basellem8  23874  basellem9  23875  chtge0  23899  chtublem  23999  logexprlim  24013  perfectlem1  24017  bcmax  24066  bposlem1  24072  bposlem2  24073  bposlem6  24077  bposlem7  24078  lgsdilem2  24119  lgsqrlem4  24132  lgsquadlem1  24142  2sqlem3  24154  2sqlem8  24160  2sqblem  24165  chebbnd1lem2  24168  chtppilimlem1  24171  chtppilim  24173  chto1ub  24174  vmadivsum  24180  rplogsumlem1  24182  rplogsumlem2  24183  dchrisum0lem1a  24184  rpvmasumlem  24185  dchrisumlem1  24187  dchrisumlem2  24188  dchrvmasumlem2  24196  dchrisum0flblem1  24206  dchrisum0flblem2  24207  dchrisum0lem1b  24213  dchrisum0lem1  24214  dchrisum0lem2a  24215  dchrisum0lem3  24217  dchrisum0  24218  mudivsum  24228  mulogsumlem  24229  mulog2sumlem1  24232  mulog2sumlem2  24233  2vmadivsumlem  24238  chpdifbndlem1  24251  selberg3lem1  24255  selberg4lem1  24258  pntrlog2bndlem1  24275  pntrlog2bndlem2  24276  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntpbnd1a  24283  pntpbnd1  24284  pntpbnd2  24285  pntibndlem2  24289  pntibndlem3  24290  pntlemd  24292  pntlemc  24293  pntlemb  24295  pntlemg  24296  pntlemh  24297  pntlemr  24300  pntlemf  24303  pntlemo  24305  abvcxp  24313  ostth2lem1  24316  padicabv  24328  ostth2lem2  24332  ostth2lem3  24333  ostth2lem4  24334  ostth2  24335  ostth3  24336  legso  24501  krippenlem  24589  midex  24633  oppperpex  24649  ttgcontlem1  24758  axpaschlem  24813  axcontlem8  24844  umgraex  24893  wwlkextproplem3  25313  clwlkisclwwlk2  25360  clwwlkndivn  25407  clwlkf1clwwlklem1  25416  ex-ind-dvds  25741  nvabs  26144  nmooge0  26250  nmoolb  26254  siii  26336  minvecolem2  26359  minvecolem4  26364  minvecolem5  26365  hlipgt0  26398  normge0  26611  normpyc  26631  pjhthlem1  26876  pjige0i  27175  nmoplb  27392  nmfnlb  27409  branmfn  27590  pjssdif2i  27659  stlei  27725  xlt2addrd  28176  eliccelico  28192  elicoelioo  28193  bcm1n  28204  2sqmod  28244  omndmul2  28310  archirngz  28341  archiabllem2c  28347  xrge0tsmsd  28384  ofldchr  28413  psgnfzto1stlem  28449  madjusmdetlem2  28490  locfinreflem  28503  xrge0iifiso  28577  nexple  28667  gsumesum  28716  esumcst  28720  esumpcvgval  28735  esumcvg  28743  esumiun  28751  measssd  28873  measunl  28874  omssubadd  28958  carsgclctunlem3  28978  pmeasmono  28982  sibfof  28998  oddpwdc  29010  eulerpartlemgc  29018  iwrdsplit  29043  ballotlemsgt1  29166  ballotlemsel1i  29168  sgnmul  29198  signsply0  29225  signstfvc  29248  signsvtp  29257  signsvfpn  29259  subfaclim  29696  erdszelem7  29705  erdszelem8  29706  cvmliftlem2  29794  snmlff  29837  sinccvglem  30101  climlec3  30153  faclim  30166  dvdspw  30170  nodense  30360  nobndup  30371  fnejoin1  30806  poimirlem12  31656  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem23  31667  poimirlem28  31672  broucube  31678  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  itg2addnclem  31697  itg2addnclem3  31699  itg2gt0cn  31701  itggt0cn  31718  ftc1anclem5  31725  ftc1anclem7  31727  ftc1anclem8  31728  isbnd3  31820  ssbnd  31824  heiborlem8  31854  bfplem2  31859  rrncmslem  31868  rrnequiv  31871  rrntotbnd  31872  lcv1  32316  lsatcv0eq  32322  lsatcvat3  32327  cvlsupr2  32618  hlatlej2  32650  cvrval4N  32688  cvratlem  32695  atcvr0eq  32700  2atlt  32713  atbtwnex  32722  athgt  32730  1cvrat  32750  ps-1  32751  hlatexch3N  32754  hlatexch4  32755  3atlem2  32758  atcvrlln2  32793  lplnexllnN  32838  4atlem3a  32871  4atlem10b  32879  4atlem11b  32882  4atlem12b  32885  2lplnja  32893  dalemply  32928  dalemsly  32929  dalem1  32933  dalem6  32942  dalem7  32943  dalem-cly  32945  dalem11  32948  dalem12  32949  dalem16  32953  dalem17  32954  dalem38  32984  dalem44  32990  dalem61  33007  lnatexN  33053  lncvrat  33056  lncmp  33057  paddasslem2  33095  dalawlem3  33147  dalawlem6  33150  dalawlem11  33155  lhpmcvr  33297  lhp2atne  33308  lhp2at0ne  33310  lautj  33367  trlval4  33463  cdlemc2  33467  cdlemc5  33470  cdleme3b  33504  cdleme11c  33536  cdleme19a  33579  cdleme20j  33594  cdleme22f  33622  cdleme23c  33627  cdleme26f2ALTN  33640  cdleme26f2  33641  cdleme35fnpq  33725  cdleme48bw  33778  cdlemg10a  33916  cdlemg11b  33918  cdlemg17g  33943  cdlemg18c  33956  cdlemi1  34094  cdlemk52  34230  dia2dimlem1  34341  dihord1  34495  dihjatcclem4  34698  eldioph2lem1  35311  lzenom  35321  irrapxlem1  35376  irrapxlem4  35379  irrapxlem5  35380  pell14qrgt0  35415  pell1qrge1  35426  pell1qrgap  35430  pellfundge  35440  pellfundex  35444  pellfund14  35456  rmspecsqrtnq  35464  rmxypos  35507  ltrmynn0  35508  ltrmxnn0  35509  jm2.24nn  35519  jm2.17b  35521  jm2.17c  35522  jm2.24  35523  congadd  35526  congsym  35528  congneg  35529  congid  35531  mzpcong  35532  acongrep  35540  acongeq  35543  jm2.18  35553  jm2.19  35558  jm2.23  35561  jm2.25  35564  jm2.26lem3  35566  jm2.15nn0  35568  jm2.16nn0  35569  jm2.27a  35570  jm2.27c  35572  jm3.1lem1  35582  idomrootle  35772  idomsubgmo  35775  inductionexd  36234  imo72b2  36260  dvgrat  36302  radcnvrat  36304  binomcxplemnn0  36339  binomcxplemnotnn0  36346  cncmpmax  36997  zltlesub  37108  lt2addmuld  37112  fmul01  37234  fmul01lt1lem1  37238  climdivf  37268  sumnnodd  37286  dvdivbd  37371  volge0  37411  stoweidlem1  37434  stoweidlem16  37449  stoweidlem18  37451  stoweidlem24  37457  stoweidlem26  37459  stoweidlem36  37470  stoweidlem38  37472  stoweidlem41  37475  stoweidlem42  37476  stoweidlem44  37478  stoweidlem45  37479  stoweidlem48  37482  stoweidlem62  37496  stoweidlem62OLD  37497  wallispilem5  37504  stirlinglem1  37509  stirlinglem5  37513  stirlinglem7  37515  stirlinglem8  37516  stirlinglem9  37517  stirlinglem11  37519  fourierdlem4  37546  fourierdlem10  37552  fourierdlem37  37579  fourierdlem47  37589  fourierdlem72  37614  fourierdlem74  37616  fourierdlem79  37621  fourierdlem82  37624  fourierdlem89  37631  fourierdlem91  37633  fourierdlem93  37635  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  etransclem24  37694  etransclem25  37695  etransclem28  37698  etransclem37  37707  etransclem38  37708  etransclem44  37714  rlimdmafv  38082  iccpartgtprec  38137  iccpartlt  38141  iccpartgtl  38143  perfectALTVlem1  38246  2elfz2melfz  38420  usgedgleord  38502  cznnring  38729  rhmsubcrngc  38802  altgsumbcALT  38907  expnegico01  39088  flnn0div2ge  39114  rege1logbrege0  39143  fllogbd  39145  fllog2  39153  nnpw2blen  39165  nnolog2flm1  39175  dignn0ldlem  39187  dignn0flhalflem1  39200  dignn0flhalflem2  39201
  Copyright terms: Public domain W3C validator