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

Theorem breqtrrd 4422
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 2477 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4420 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452   class class class wbr 4395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396
This theorem is referenced by:  marypha1lem  7965  marypha2  7971  unxpwdom  8122  uncdadom  8619  cdacomen  8629  cdaassen  8630  xpcdaen  8631  onacda  8645  infcdaabs  8654  cfss  8713  tskuni  9226  ltexnq  9418  lt2addmuld  10885  mul2lt0rgt0  11422  xrmax1  11493  xrmax2  11494  max1ALT  11504  qbtwnxr  11516  xleadd1a  11564  xlt2add  11571  xlesubadd  11574  xmulgt0  11594  xlemul1a  11599  xov1plusxeqvd  11804  uzsubsubfz  11847  fzctr  11928  subfzo0  12058  flflp1  12076  ceilge  12106  modge0  12139  modlt  12140  modid  12154  modaddmodup  12187  sermono  12283  seqf1olem1  12290  seqf1olem2  12291  leexp1a  12369  sqgt0  12381  sqge0  12389  nnlesq  12416  expnbnd  12439  expmulnbnd  12442  discr1  12446  facwordi  12512  faclbnd5  12521  hashdom  12596  fi1uzind  12691  brfi1indALT  12694  fi1uzindOLD  12697  brfi1indALTOLD  12700  ccatws1n0  12819  swrds2  13092  cjmulge0  13286  resqrtcl  13394  absge0  13427  sqreulem  13499  amgm2  13509  rlimdm  13692  rlimge0  13722  reccn2  13737  climle  13780  climserle  13803  isercoll2  13809  iseraltlem1  13825  iseralt  13828  isumclim2  13896  isumclim3  13897  isumge0  13904  fsumless  13933  cvgcmp  13953  cvgcmpce  13955  abscvgcvg  13956  isumsup2  13981  isumltss  13983  climcndslem1  13984  climcnds  13986  supcvg  13991  harmonic  13994  expcnv  13999  explecnv  14000  cvgrat  14016  mertenslem1  14017  mertenslem2  14018  clim2div  14022  ntrivcvgtail  14033  iprodclim2  14129  iprodclim3  14130  efcvg  14216  ege2le3  14221  efaddlem  14224  eftlub  14240  effsumlt  14242  tanhlt1  14291  ef01bndlem  14315  sin02gt0  14323  rpnnen2lem4  14347  ruclem2  14361  ruclem3  14362  ruclem9  14367  iddvdsexp  14403  dvdsadd  14420  dvdsfac  14438  dvdsmod  14440  3dvds  14448  divalglem1  14451  bitsfzo  14488  bitsmod  14489  bitscmp  14491  bitsinv1lem  14494  sadcaddlem  14510  sadadd3  14514  sadaddlem  14519  dvdssqim  14600  dvdsmulgcd  14601  nn0seqcvgd  14608  dvdslcm  14642  lcmgcdlem  14650  dvdslcmf  14683  lcmfunsnlem2lem2  14691  sqnprm  14725  mulgcddvds  14740  qredeq  14742  isprm6  14745  nonsq  14787  hashdvds  14802  prmdiv  14812  odzdvds  14819  odzdvdsOLD  14825  omoe  14841  pythagtriplem4  14848  pcpre1  14871  pcdvdsb  14897  pcz  14909  pcprmpw2  14910  pcaddlem  14912  pcadd  14913  pcadd2  14914  pcmpt  14916  pcmptdvds  14918  fldivp1  14921  pcfaclem  14922  pockthlem  14928  prmreclem1  14939  prmreclem3  14941  prmreclem5  14943  prmreclem6  14944  4sqlem6  14966  4sqlem8  14968  4sqlem11  14978  4sqlem12  14979  4sqlem14OLD  14981  4sqlem16OLD  14983  4sqlem14  14987  4sqlem16  14989  vdwlem3  15012  vdwlem9  15018  vdwlem10  15019  vdwlem12  15021  ramub1lem2  15064  prmorlefacOLD  15097  prmgap  15108  prmgaplcmOLD  15109  prmgaplcm  15110  prmgapprmo  15112  invfuc  15957  ple1  16368  eqgen  16948  lagsubg  16957  pgpfi  17335  sylow2alem2  17348  sylow2a  17349  sylow3lem4  17360  efgsrel  17462  odadd1  17564  odadd2  17565  gexex  17569  lt6abl  17607  dprd2d2  17755  dmdprdpr  17760  ablfacrp2  17778  ablfac1c  17782  pgpfaclem1  17792  ablfac2  17800  dvdsrmul1  17959  unitmulclb  17971  subrguss  18101  abvres  18145  ply1coefsupp  18965  evl1gsumadd  19023  znfld  19208  znunit  19211  frlmisfrlm  19483  matgsum  19539  pm2mpcl  19898  psmetxrge0  21407  isxmet2d  21420  mettri  21445  xmettri3  21446  mettri3  21447  xmetrtri2  21449  prdsxmetlem  21461  imasdsf1olem  21466  xblss2ps  21494  blss2ps  21496  blss2  21497  blssps  21517  blss  21518  prdsbl  21584  dscmet  21665  nmge0  21708  nmmtri  21713  nlmvscnlem2  21766  nrginvrcnlem  21771  nmoix  21812  nmoleub  21814  nmoixOLD  21828  nmoleubOLD  21830  blcvx  21894  xrsxmet  21905  opnreen  21927  xrge0tsms  21930  icopnfcnv  22048  xrhmeo  22052  lebnumii  22075  pcophtb  22138  pi1grplem  22158  nmoleub2lem  22206  ipcau2  22286  tchcphlem1  22287  ipcau  22290  ipcnlem2  22293  rrxcph  22429  minveclem2  22446  minveclem3b  22448  minveclem2OLD  22458  minveclem3bOLD  22460  pjthlem1  22469  pjthlem2  22470  ivthlem3  22482  ivth2  22484  ovolfsf  22502  ovolsslem  22515  ovollb2lem  22519  ovollb2  22520  ovolctb  22521  ovolfiniun  22532  ovolicc1  22547  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2  22554  nulmbl2  22568  unmbl  22569  ioombl1lem4  22593  uniioombllem4  22623  uniioombllem6  22625  volivth  22644  vitalilem4  22648  itg1ge0  22723  itg1ge0a  22748  itg1lea  22749  itg1climres  22751  mbfi1fseqlem5  22756  itg2ub  22770  itg2seq  22779  itg2uba  22780  itg2splitlem  22785  itg2split  22786  itg2monolem3  22789  itg2mono  22790  itg2i1fseq2  22793  itg2addlem  22795  iblss  22841  itggt0  22878  dvferm2lem  23017  dvlip  23024  dvivthlem1  23039  dvfsumlem2  23058  dvfsumlem3  23059  ftc1lem4  23070  ply1divmo  23165  ply1remlem  23192  fta1glem2  23196  ig1pdvds  23207  ig1pdvdsOLD  23213  plyeq0lem  23243  plydiveu  23330  fta1lem  23339  vieta1lem2  23343  aaliou3lem2  23378  aaliou3lem8  23380  ulmcn  23433  mtest  23438  itgulm  23442  radcnvlem1  23447  radcnvlt1  23452  dvradcnv  23455  pserdvlem2  23462  abelthlem2  23466  abelthlem6  23470  abelthlem7  23472  abelthlem9  23474  tangtx  23539  sinq12gt0  23541  sineq0  23555  cosordlem  23559  tanord  23566  tanregt0  23567  logrnaddcl  23603  logcj  23634  argregt0  23638  argrege0  23639  argimgt0  23640  argimlt0  23641  logimul  23642  logneg2  23643  logdivlti  23648  divlogrlim  23659  logcnlem3  23668  logcnlem4  23669  dvlog2lem  23676  logtayl  23684  rpcxpcl  23700  cxpsqrtlem  23726  cxpaddle  23771  isosctrlem1  23826  asinlem3a  23875  asinlem3  23876  asinneg  23891  asinsinlem  23896  asinsin  23897  atanlogaddlem  23918  atanlogadd  23919  atanlogsublem  23920  atanlogsub  23921  atantan  23928  atanbndlem  23930  atantayl  23942  leibpi  23947  birthdaylem3  23958  areaf  23966  cxploglim  23982  jensenlem2  23992  jensen  23993  logdiflbnd  23999  harmonicbnd4  24015  fsumharmonic  24016  zetacvg  24019  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamcvg2  24059  wilthlem2  24073  ftalem1  24076  ftalem2  24077  ftalem5  24080  ftalem5OLD  24082  basellem6  24091  basellem8  24093  basellem9  24094  chtge0  24118  chtublem  24218  logexprlim  24232  perfectlem1  24236  bcmax  24285  bposlem1  24291  bposlem2  24292  bposlem6  24296  bposlem7  24297  lgsdilem2  24338  lgsqrlem4  24351  lgsquadlem1  24361  2sqlem3  24373  2sqlem8  24379  2sqblem  24384  chebbnd1lem2  24387  chtppilimlem1  24390  chtppilim  24392  chto1ub  24393  vmadivsum  24399  rplogsumlem1  24401  rplogsumlem2  24402  dchrisum0lem1a  24403  rpvmasumlem  24404  dchrisumlem1  24406  dchrisumlem2  24407  dchrvmasumlem2  24415  dchrisum0flblem1  24425  dchrisum0flblem2  24426  dchrisum0lem1b  24432  dchrisum0lem1  24433  dchrisum0lem2a  24434  dchrisum0lem3  24436  dchrisum0  24437  mudivsum  24447  mulogsumlem  24448  mulog2sumlem1  24451  mulog2sumlem2  24452  2vmadivsumlem  24457  chpdifbndlem1  24470  selberg3lem1  24474  selberg4lem1  24477  pntrlog2bndlem1  24494  pntrlog2bndlem2  24495  pntrlog2bndlem3  24496  pntrlog2bndlem4  24497  pntpbnd1a  24502  pntpbnd1  24503  pntpbnd2  24504  pntibndlem2  24508  pntibndlem3  24509  pntlemd  24511  pntlemc  24512  pntlemb  24514  pntlemg  24515  pntlemh  24516  pntlemr  24519  pntlemf  24522  pntlemo  24524  abvcxp  24532  ostth2lem1  24535  padicabv  24547  ostth2lem2  24551  ostth2lem3  24552  ostth2lem4  24553  ostth2  24554  ostth3  24555  tgcgr4  24655  legso  24723  krippenlem  24814  midex  24858  oppperpex  24874  ttgcontlem1  24994  axpaschlem  25049  axcontlem8  25080  umgraex  25129  wwlkextproplem3  25550  clwlkisclwwlk2  25597  clwwlkndivn  25644  clwlkf1clwwlklem1  25653  ex-ind-dvds  25978  nvabs  26383  nmooge0  26489  nmoolb  26493  siii  26575  minvecolem2  26598  minvecolem4  26603  minvecolem5  26604  minvecolem2OLD  26608  minvecolem4OLD  26613  minvecolem5OLD  26614  hlipgt0  26647  normge0  26860  normpyc  26880  pjhthlem1  27125  pjige0i  27424  nmoplb  27641  nmfnlb  27658  branmfn  27839  pjssdif2i  27908  stlei  27974  xlt2addrd  28413  eliccelico  28434  elicoelioo  28435  bcm1n  28446  2sqmod  28484  omndmul2  28549  archirngz  28580  archiabllem2c  28586  xrge0tsmsd  28622  ofldchr  28651  psgnfzto1stlem  28687  madjusmdetlem2  28728  locfinreflem  28741  xrge0iifiso  28815  nexple  28905  gsumesum  28954  esumcst  28958  esumpcvgval  28973  esumcvg  28981  esumiun  28989  measssd  29111  measunl  29112  omssubadd  29201  omssubaddOLD  29205  carsgclctunlem3  29225  pmeasmono  29230  sibfof  29246  oddpwdc  29260  eulerpartlemgc  29268  iwrdsplit  29293  ballotlemsgt1  29416  ballotlemsel1i  29418  ballotlemsgt1OLD  29454  ballotlemsel1iOLD  29456  sgnmul  29486  signsply0  29512  signstfvc  29535  signsvtp  29544  signsvfpn  29546  subfaclim  29983  erdszelem7  29992  erdszelem8  29993  cvmliftlem2  30081  snmlff  30124  sinccvglem  30388  climlec3  30440  faclim  30453  dvdspw  30457  nodense  30649  nobndup  30660  fnejoin1  31095  poimirlem12  32016  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem23  32027  poimirlem28  32032  broucube  32038  mblfinlem2  32042  mblfinlem3  32043  mblfinlem4  32044  ismblfin  32045  itg2addnclem  32057  itg2addnclem3  32059  itg2gt0cn  32061  itggt0cn  32078  ftc1anclem5  32085  ftc1anclem7  32087  ftc1anclem8  32088  isbnd3  32180  ssbnd  32184  heiborlem8  32214  bfplem2  32219  rrncmslem  32228  rrnequiv  32231  rrntotbnd  32232  lcv1  32678  lsatcv0eq  32684  lsatcvat3  32689  cvlsupr2  32980  hlatlej2  33012  cvrval4N  33050  cvratlem  33057  atcvr0eq  33062  2atlt  33075  atbtwnex  33084  athgt  33092  1cvrat  33112  ps-1  33113  hlatexch3N  33116  hlatexch4  33117  3atlem2  33120  atcvrlln2  33155  lplnexllnN  33200  4atlem3a  33233  4atlem10b  33241  4atlem11b  33244  4atlem12b  33247  2lplnja  33255  dalemply  33290  dalemsly  33291  dalem1  33295  dalem6  33304  dalem7  33305  dalem-cly  33307  dalem11  33310  dalem12  33311  dalem16  33315  dalem17  33316  dalem38  33346  dalem44  33352  dalem61  33369  lnatexN  33415  lncvrat  33418  lncmp  33419  paddasslem2  33457  dalawlem3  33509  dalawlem6  33512  dalawlem11  33517  lhpmcvr  33659  lhp2atne  33670  lhp2at0ne  33672  lautj  33729  trlval4  33825  cdlemc2  33829  cdlemc5  33832  cdleme3b  33866  cdleme11c  33898  cdleme19a  33941  cdleme20j  33956  cdleme22f  33984  cdleme23c  33989  cdleme26f2ALTN  34002  cdleme26f2  34003  cdleme35fnpq  34087  cdleme48bw  34140  cdlemg10a  34278  cdlemg11b  34280  cdlemg17g  34305  cdlemg18c  34318  cdlemi1  34456  cdlemk52  34592  dia2dimlem1  34703  dihord1  34857  dihjatcclem4  35060  eldioph2lem1  35673  lzenom  35683  irrapxlem1  35737  irrapxlem4  35740  irrapxlem5  35741  pell14qrgt0  35776  pell1qrge1  35787  pell1qrgap  35791  pellfundge  35801  pellfundex  35805  pellfund14  35817  rmspecsqrtnq  35825  rmxypos  35868  ltrmynn0  35869  ltrmxnn0  35870  jm2.24nn  35880  jm2.17b  35882  jm2.17c  35883  jm2.24  35884  congadd  35887  congsym  35889  congneg  35890  congid  35892  mzpcong  35893  acongrep  35901  acongeq  35904  jm2.18  35914  jm2.19  35919  jm2.23  35922  jm2.25  35925  jm2.26lem3  35927  jm2.15nn0  35929  jm2.16nn0  35930  jm2.27a  35931  jm2.27c  35933  jm3.1lem1  35943  idomrootle  36140  idomsubgmo  36143  inductionexd  36664  imo72b2  36689  dvgrat  36731  radcnvrat  36733  binomcxplemnn0  36768  binomcxplemnotnn0  36775  cncmpmax  37416  zltlesub  37585  fmul01  37755  fmul01lt1lem1  37759  climdivf  37789  sumnnodd  37807  dvdivbd  37892  volge0  37935  stoweidlem1  37973  stoweidlem16  37988  stoweidlem18  37990  stoweidlem24  37996  stoweidlem26  37998  stoweidlem36  38009  stoweidlem38  38011  stoweidlem41  38014  stoweidlem42  38015  stoweidlem44  38017  stoweidlem45  38018  stoweidlem48  38021  stoweidlem62  38035  stoweidlem62OLD  38036  wallispilem5  38043  stirlinglem1  38048  stirlinglem5  38052  stirlinglem7  38054  stirlinglem8  38055  stirlinglem9  38056  stirlinglem11  38058  fourierdlem4  38085  fourierdlem10  38091  fourierdlem37  38119  fourierdlem47  38129  fourierdlem72  38154  fourierdlem74  38156  fourierdlem79  38161  fourierdlem82  38164  fourierdlem89  38171  fourierdlem91  38173  fourierdlem93  38175  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  etransclem24  38235  etransclem25  38236  etransclem28  38239  etransclem37  38248  etransclem38  38249  etransclem44  38255  rlimdmafv  38824  iccpartgtprec  38879  iccpartlt  38883  iccpartgtl  38885  perfectALTVlem1  38988  2elfz2melfz  39203  nfile  39217  upgrex  39338  nbfusgrlevtxm1  39615  usgedgleord  40239  cznnring  40466  rhmsubcrngc  40539  altgsumbcALT  40642  expnegico01  40823  flnn0div2ge  40848  rege1logbrege0  40877  fllogbd  40879  fllog2  40887  nnpw2blen  40899  nnolog2flm1  40909  dignn0ldlem  40921  dignn0flhalflem1  40934  dignn0flhalflem2  40935
  Copyright terms: Public domain W3C validator