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

Theorem breqtrrd 4429
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 2457 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4427 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444   class class class wbr 4402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403
This theorem is referenced by:  marypha1lem  7947  marypha2  7953  unxpwdom  8104  uncdadom  8601  cdacomen  8611  cdaassen  8612  xpcdaen  8613  onacda  8627  infcdaabs  8636  cfss  8695  tskuni  9208  ltexnq  9400  mul2lt0rgt0  11399  xrmax1  11470  xrmax2  11471  max1ALT  11481  qbtwnxr  11493  xleadd1a  11539  xlt2add  11546  xlesubadd  11549  xmulgt0  11569  xlemul1a  11574  xov1plusxeqvd  11778  uzsubsubfz  11821  fzctr  11903  flflp1  12043  ceilge  12073  modge0  12106  modlt  12107  modid  12121  modaddmodup  12153  sermono  12245  seqf1olem1  12252  seqf1olem2  12253  leexp1a  12331  sqgt0  12343  sqge0  12351  nnlesq  12378  expnbnd  12401  expmulnbnd  12404  discr1  12408  facwordi  12474  faclbnd5  12483  hashdom  12558  fi1uzind  12650  brfi1indALT  12653  ccatws1n0  12765  swrds2  13020  cjmulge0  13209  resqrtcl  13317  absge0  13350  sqreulem  13422  amgm2  13432  rlimdm  13615  rlimge0  13645  reccn2  13660  climle  13703  climserle  13726  isercoll2  13732  iseraltlem1  13748  iseralt  13751  isumclim2  13819  isumclim3  13820  isumge0  13827  fsumless  13856  cvgcmp  13876  cvgcmpce  13878  abscvgcvg  13879  isumsup2  13904  isumltss  13906  climcndslem1  13907  climcnds  13909  supcvg  13914  harmonic  13917  expcnv  13922  explecnv  13923  cvgrat  13939  mertenslem1  13940  mertenslem2  13941  clim2div  13945  ntrivcvgtail  13956  iprodclim2  14052  iprodclim3  14053  efcvg  14139  ege2le3  14144  efaddlem  14147  eftlub  14163  effsumlt  14165  tanhlt1  14214  ef01bndlem  14238  sin02gt0  14246  rpnnen2lem4  14270  ruclem2  14284  ruclem3  14285  ruclem9  14290  iddvdsexp  14326  dvdsadd  14343  dvdsfac  14360  dvdsmod  14362  3dvds  14369  divalglem1  14372  bitsfzo  14409  bitsmod  14410  bitscmp  14412  bitsinv1lem  14415  sadcaddlem  14431  sadadd3  14435  sadaddlem  14440  dvdssqim  14521  dvdsmulgcd  14522  nn0seqcvgd  14529  dvdslcm  14563  lcmgcdlem  14571  dvdslcmf  14604  lcmfunsnlem2lem2  14612  sqnprm  14646  mulgcddvds  14661  qredeq  14663  isprm6  14666  nonsq  14708  hashdvds  14723  prmdiv  14733  odzdvds  14740  odzdvdsOLD  14746  omoe  14762  pythagtriplem4  14769  pcpre1  14792  pcdvdsb  14818  pcz  14830  pcprmpw2  14831  pcaddlem  14833  pcadd  14834  pcadd2  14835  pcmpt  14837  pcmptdvds  14839  fldivp1  14842  pcfaclem  14843  pockthlem  14849  prmreclem1  14860  prmreclem3  14862  prmreclem5  14864  prmreclem6  14865  4sqlem6  14887  4sqlem8  14889  4sqlem11  14899  4sqlem12  14900  4sqlem14OLD  14902  4sqlem16OLD  14904  4sqlem14  14908  4sqlem16  14910  vdwlem3  14933  vdwlem9  14939  vdwlem10  14940  vdwlem12  14942  ramub1lem2  14985  prmorlefacOLD  15018  prmgap  15029  prmgaplcmOLD  15030  prmgaplcm  15031  prmgapprmo  15033  invfuc  15879  ple1  16290  eqgen  16870  lagsubg  16879  pgpfi  17257  sylow2alem2  17270  sylow2a  17271  sylow3lem4  17282  efgsrel  17384  odadd1  17486  odadd2  17487  gexex  17491  lt6abl  17529  dprd2d2  17677  dmdprdpr  17682  ablfacrp2  17700  ablfac1c  17704  pgpfaclem1  17714  ablfac2  17722  dvdsrmul1  17881  unitmulclb  17893  subrguss  18023  abvres  18067  ply1coefsupp  18888  evl1gsumadd  18946  znfld  19131  znunit  19134  frlmisfrlm  19406  matgsum  19462  pm2mpcl  19821  psmetxrge0  21329  isxmet2d  21342  mettri  21367  xmettri3  21368  mettri3  21369  xmetrtri2  21371  prdsxmetlem  21383  imasdsf1olem  21388  xblss2ps  21416  blss2ps  21418  blss2  21419  blssps  21439  blss  21440  prdsbl  21506  dscmet  21587  nmge0  21630  nmmtri  21635  nlmvscnlem2  21688  nrginvrcnlem  21693  nmoix  21734  nmoleub  21736  nmoixOLD  21750  nmoleubOLD  21752  blcvx  21816  xrsxmet  21827  opnreen  21849  xrge0tsms  21852  icopnfcnv  21970  xrhmeo  21974  lebnumii  21997  pcophtb  22060  pi1grplem  22080  nmoleub2lem  22128  ipcau2  22208  tchcphlem1  22209  ipcau  22212  ipcnlem2  22215  rrxcph  22351  minveclem2  22368  minveclem3b  22370  minveclem2OLD  22380  minveclem3bOLD  22382  pjthlem1  22391  pjthlem2  22392  ivthlem3  22404  ivth2  22406  ovolfsf  22424  ovolsslem  22437  ovollb2lem  22441  ovollb2  22442  ovolctb  22443  ovolfiniun  22454  ovolicc1  22469  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ovolicc2  22476  nulmbl2  22490  unmbl  22491  ioombl1lem4  22514  uniioombllem4  22544  uniioombllem6  22546  volivth  22565  vitalilem4  22569  itg1ge0  22644  itg1ge0a  22669  itg1lea  22670  itg1climres  22672  mbfi1fseqlem5  22677  itg2ub  22691  itg2seq  22700  itg2uba  22701  itg2splitlem  22706  itg2split  22707  itg2monolem3  22710  itg2mono  22711  itg2i1fseq2  22714  itg2addlem  22716  iblss  22762  itggt0  22799  dvferm2lem  22938  dvlip  22945  dvivthlem1  22960  dvfsumlem2  22979  dvfsumlem3  22980  ftc1lem4  22991  ply1divmo  23086  ply1remlem  23113  fta1glem2  23117  ig1pdvds  23128  ig1pdvdsOLD  23134  plyeq0lem  23164  plydiveu  23251  fta1lem  23260  vieta1lem2  23264  aaliou3lem2  23299  aaliou3lem8  23301  ulmcn  23354  mtest  23359  itgulm  23363  radcnvlem1  23368  radcnvlt1  23373  dvradcnv  23376  pserdvlem2  23383  abelthlem2  23387  abelthlem6  23391  abelthlem7  23393  abelthlem9  23395  tangtx  23460  sinq12gt0  23462  sineq0  23476  cosordlem  23480  tanord  23487  tanregt0  23488  logrnaddcl  23524  logcj  23555  argregt0  23559  argrege0  23560  argimgt0  23561  argimlt0  23562  logimul  23563  logneg2  23564  logdivlti  23569  divlogrlim  23580  logcnlem3  23589  logcnlem4  23590  dvlog2lem  23597  logtayl  23605  rpcxpcl  23621  cxpsqrtlem  23647  cxpaddle  23692  isosctrlem1  23747  asinlem3a  23796  asinlem3  23797  asinneg  23812  asinsinlem  23817  asinsin  23818  atanlogaddlem  23839  atanlogadd  23840  atanlogsublem  23841  atanlogsub  23842  atantan  23849  atanbndlem  23851  atantayl  23863  leibpi  23868  birthdaylem3  23879  areaf  23887  cxploglim  23903  jensenlem2  23913  jensen  23914  logdiflbnd  23920  harmonicbnd4  23936  fsumharmonic  23937  zetacvg  23940  lgamgulmlem2  23955  lgamgulmlem3  23956  lgamcvg2  23980  wilthlem2  23994  ftalem1  23997  ftalem2  23998  ftalem5  24001  ftalem5OLD  24003  basellem6  24012  basellem8  24014  basellem9  24015  chtge0  24039  chtublem  24139  logexprlim  24153  perfectlem1  24157  bcmax  24206  bposlem1  24212  bposlem2  24213  bposlem6  24217  bposlem7  24218  lgsdilem2  24259  lgsqrlem4  24272  lgsquadlem1  24282  2sqlem3  24294  2sqlem8  24300  2sqblem  24305  chebbnd1lem2  24308  chtppilimlem1  24311  chtppilim  24313  chto1ub  24314  vmadivsum  24320  rplogsumlem1  24322  rplogsumlem2  24323  dchrisum0lem1a  24324  rpvmasumlem  24325  dchrisumlem1  24327  dchrisumlem2  24328  dchrvmasumlem2  24336  dchrisum0flblem1  24346  dchrisum0flblem2  24347  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2a  24355  dchrisum0lem3  24357  dchrisum0  24358  mudivsum  24368  mulogsumlem  24369  mulog2sumlem1  24372  mulog2sumlem2  24373  2vmadivsumlem  24378  chpdifbndlem1  24391  selberg3lem1  24395  selberg4lem1  24398  pntrlog2bndlem1  24415  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntpbnd1a  24423  pntpbnd1  24424  pntpbnd2  24425  pntibndlem2  24429  pntibndlem3  24430  pntlemd  24432  pntlemc  24433  pntlemb  24435  pntlemg  24436  pntlemh  24437  pntlemr  24440  pntlemf  24443  pntlemo  24445  abvcxp  24453  ostth2lem1  24456  padicabv  24468  ostth2lem2  24472  ostth2lem3  24473  ostth2lem4  24474  ostth2  24475  ostth3  24476  tgcgr4  24576  legso  24644  krippenlem  24735  midex  24779  oppperpex  24795  ttgcontlem1  24915  axpaschlem  24970  axcontlem8  25001  umgraex  25050  wwlkextproplem3  25471  clwlkisclwwlk2  25518  clwwlkndivn  25565  clwlkf1clwwlklem1  25574  ex-ind-dvds  25899  nvabs  26302  nmooge0  26408  nmoolb  26412  siii  26494  minvecolem2  26517  minvecolem4  26522  minvecolem5  26523  minvecolem2OLD  26527  minvecolem4OLD  26532  minvecolem5OLD  26533  hlipgt0  26566  normge0  26779  normpyc  26799  pjhthlem1  27044  pjige0i  27343  nmoplb  27560  nmfnlb  27577  branmfn  27758  pjssdif2i  27827  stlei  27893  xlt2addrd  28338  eliccelico  28359  elicoelioo  28360  bcm1n  28371  2sqmod  28409  omndmul2  28475  archirngz  28506  archiabllem2c  28512  xrge0tsmsd  28548  ofldchr  28577  psgnfzto1stlem  28613  madjusmdetlem2  28654  locfinreflem  28667  xrge0iifiso  28741  nexple  28831  gsumesum  28880  esumcst  28884  esumpcvgval  28899  esumcvg  28907  esumiun  28915  measssd  29037  measunl  29038  omssubadd  29128  omssubaddOLD  29132  carsgclctunlem3  29152  pmeasmono  29157  sibfof  29173  oddpwdc  29187  eulerpartlemgc  29195  iwrdsplit  29220  ballotlemsgt1  29343  ballotlemsel1i  29345  ballotlemsgt1OLD  29381  ballotlemsel1iOLD  29383  sgnmul  29413  signsply0  29440  signstfvc  29463  signsvtp  29472  signsvfpn  29474  subfaclim  29911  erdszelem7  29920  erdszelem8  29921  cvmliftlem2  30009  snmlff  30052  sinccvglem  30316  climlec3  30369  faclim  30382  dvdspw  30386  nodense  30578  nobndup  30589  fnejoin1  31024  poimirlem12  31952  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem23  31963  poimirlem28  31968  broucube  31974  mblfinlem2  31978  mblfinlem3  31979  mblfinlem4  31980  ismblfin  31981  itg2addnclem  31993  itg2addnclem3  31995  itg2gt0cn  31997  itggt0cn  32014  ftc1anclem5  32021  ftc1anclem7  32023  ftc1anclem8  32024  isbnd3  32116  ssbnd  32120  heiborlem8  32150  bfplem2  32155  rrncmslem  32164  rrnequiv  32167  rrntotbnd  32168  lcv1  32607  lsatcv0eq  32613  lsatcvat3  32618  cvlsupr2  32909  hlatlej2  32941  cvrval4N  32979  cvratlem  32986  atcvr0eq  32991  2atlt  33004  atbtwnex  33013  athgt  33021  1cvrat  33041  ps-1  33042  hlatexch3N  33045  hlatexch4  33046  3atlem2  33049  atcvrlln2  33084  lplnexllnN  33129  4atlem3a  33162  4atlem10b  33170  4atlem11b  33173  4atlem12b  33176  2lplnja  33184  dalemply  33219  dalemsly  33220  dalem1  33224  dalem6  33233  dalem7  33234  dalem-cly  33236  dalem11  33239  dalem12  33240  dalem16  33244  dalem17  33245  dalem38  33275  dalem44  33281  dalem61  33298  lnatexN  33344  lncvrat  33347  lncmp  33348  paddasslem2  33386  dalawlem3  33438  dalawlem6  33441  dalawlem11  33446  lhpmcvr  33588  lhp2atne  33599  lhp2at0ne  33601  lautj  33658  trlval4  33754  cdlemc2  33758  cdlemc5  33761  cdleme3b  33795  cdleme11c  33827  cdleme19a  33870  cdleme20j  33885  cdleme22f  33913  cdleme23c  33918  cdleme26f2ALTN  33931  cdleme26f2  33932  cdleme35fnpq  34016  cdleme48bw  34069  cdlemg10a  34207  cdlemg11b  34209  cdlemg17g  34234  cdlemg18c  34247  cdlemi1  34385  cdlemk52  34521  dia2dimlem1  34632  dihord1  34786  dihjatcclem4  34989  eldioph2lem1  35602  lzenom  35612  irrapxlem1  35666  irrapxlem4  35669  irrapxlem5  35670  pell14qrgt0  35705  pell1qrge1  35716  pell1qrgap  35720  pellfundge  35730  pellfundex  35734  pellfund14  35746  rmspecsqrtnq  35754  rmxypos  35797  ltrmynn0  35798  ltrmxnn0  35799  jm2.24nn  35809  jm2.17b  35811  jm2.17c  35812  jm2.24  35813  congadd  35816  congsym  35818  congneg  35819  congid  35821  mzpcong  35822  acongrep  35830  acongeq  35833  jm2.18  35843  jm2.19  35848  jm2.23  35851  jm2.25  35854  jm2.26lem3  35856  jm2.15nn0  35858  jm2.16nn0  35859  jm2.27a  35860  jm2.27c  35862  jm3.1lem1  35872  idomrootle  36069  idomsubgmo  36072  inductionexd  36593  imo72b2  36619  dvgrat  36661  radcnvrat  36663  binomcxplemnn0  36698  binomcxplemnotnn0  36705  cncmpmax  37353  zltlesub  37495  lt2addmuld  37499  fmul01  37658  fmul01lt1lem1  37662  climdivf  37692  sumnnodd  37710  dvdivbd  37795  volge0  37838  stoweidlem1  37861  stoweidlem16  37876  stoweidlem18  37878  stoweidlem24  37884  stoweidlem26  37886  stoweidlem36  37897  stoweidlem38  37899  stoweidlem41  37902  stoweidlem42  37903  stoweidlem44  37905  stoweidlem45  37906  stoweidlem48  37909  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem5  37931  stirlinglem1  37936  stirlinglem5  37940  stirlinglem7  37942  stirlinglem8  37943  stirlinglem9  37944  stirlinglem11  37946  fourierdlem4  37973  fourierdlem10  37979  fourierdlem37  38007  fourierdlem47  38017  fourierdlem72  38042  fourierdlem74  38044  fourierdlem79  38049  fourierdlem82  38052  fourierdlem89  38059  fourierdlem91  38061  fourierdlem93  38063  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  etransclem24  38123  etransclem25  38124  etransclem28  38127  etransclem37  38136  etransclem38  38137  etransclem44  38143  rlimdmafv  38679  iccpartgtprec  38734  iccpartlt  38738  iccpartgtl  38740  perfectALTVlem1  38843  2elfz2melfz  39058  nfile  39067  upgrex  39184  nbfusgrlevtxm1  39451  usgedgleord  39784  cznnring  40011  rhmsubcrngc  40084  altgsumbcALT  40187  expnegico01  40368  flnn0div2ge  40393  rege1logbrege0  40422  fllogbd  40424  fllog2  40432  nnpw2blen  40444  nnolog2flm1  40454  dignn0ldlem  40466  dignn0flhalflem1  40479  dignn0flhalflem2  40480
  Copyright terms: Public domain W3C validator