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

Theorem breqtrrd 4473
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 2475 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4471 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  marypha1lem  7889  marypha2  7895  unxpwdom  8011  uncdadom  8547  cdacomen  8557  cdaassen  8558  xpcdaen  8559  onacda  8573  infcdaabs  8582  cfss  8641  tskuni  9157  ltexnq  9349  xrmax1  11372  xrmax2  11373  max1ALT  11383  qbtwnxr  11395  xleadd1a  11441  xlt2add  11448  xlesubadd  11451  xmulgt0  11471  xlemul1a  11476  xov1plusxeqvd  11662  uzsubsubfz  11703  fzctr  11780  flflp1  11908  ceilge  11937  modge0  11969  modlt  11970  modid  11984  modaddmodup  12014  sermono  12103  seqf1olem1  12110  seqf1olem2  12111  leexp1a  12188  sqgt0  12200  sqge0  12208  nnlesq  12235  expnbnd  12259  expmulnbnd  12262  discr1  12266  facwordi  12331  faclbnd5  12340  hashdom  12411  brfi1uzind  12494  ccatws1n0  12595  swrds2  12842  cjmulge0  12938  resqrtcl  13046  absge0  13079  sqreulem  13151  amgm2  13161  rlimdm  13333  rlimge0  13363  reccn2  13378  climle  13421  climserle  13444  isercoll2  13450  iseraltlem1  13463  iseralt  13466  isumclim2  13532  isumclim3  13533  isumge0  13540  fsumless  13569  cvgcmp  13589  cvgcmpce  13591  abscvgcvg  13592  isumsup2  13617  isumltss  13619  climcndslem1  13620  climcnds  13622  supcvg  13626  harmonic  13629  expcnv  13634  explecnv  13635  cvgrat  13651  mertenslem1  13652  mertenslem2  13653  efcvg  13678  ege2le3  13683  efaddlem  13686  eftlub  13701  effsumlt  13703  tanhlt1  13752  ef01bndlem  13776  sin02gt0  13784  rpnnen2lem4  13808  ruclem2  13822  ruclem3  13823  ruclem9  13828  iddvdsexp  13864  dvdsadd  13879  dvdsfac  13896  dvdsmod  13898  3dvds  13905  divalglem1  13907  bitsfzo  13940  bitsmod  13941  bitscmp  13943  bitsinv1lem  13946  sadcaddlem  13962  sadadd3  13966  sadaddlem  13971  dvdssqim  14046  dvdsmulgcd  14047  nn0seqcvgd  14054  sqnprm  14094  mulgcddvds  14100  qredeq  14102  isprm6  14105  nonsq  14147  hashdvds  14160  prmdiv  14170  odzdvds  14177  omoe  14191  pythagtriplem4  14198  pcpre1  14221  pcdvdsb  14247  pcz  14259  pcprmpw2  14260  pcaddlem  14262  pcadd  14263  pcadd2  14264  pcmpt  14266  pcmptdvds  14268  fldivp1  14271  pcfaclem  14272  pockthlem  14278  prmreclem1  14289  prmreclem3  14291  prmreclem5  14293  prmreclem6  14294  4sqlem6  14316  4sqlem8  14318  4sqlem11  14328  4sqlem12  14329  4sqlem14  14331  4sqlem16  14333  vdwlem3  14356  vdwlem9  14362  vdwlem10  14363  vdwlem12  14365  ramub1lem2  14400  invfuc  15197  ple1  15527  eqgen  16049  lagsubg  16058  pgpfi  16421  sylow2alem2  16434  sylow2a  16435  sylow3lem4  16446  efgsrel  16548  odadd1  16647  odadd2  16648  gexex  16652  lt6abl  16688  dprd2d2  16883  dmdprdpr  16888  ablfacrp2  16908  ablfac1c  16912  pgpfaclem1  16922  ablfac2  16930  dvdsrmul1  17086  unitmulclb  17098  subrguss  17227  abvres  17271  ply1coefsupp  18107  evl1gsumadd  18165  znfld  18366  znunit  18369  frlmisfrlm  18650  matgsum  18706  pm2mpcl  19065  psmetxrge0  20552  isxmet2d  20565  mettri  20590  xmettri3  20591  mettri3  20592  xmetrtri2  20594  prdsxmetlem  20606  imasdsf1olem  20611  xblss2ps  20639  blss2ps  20641  blss2  20642  blssps  20662  blss  20663  prdsbl  20729  dscmet  20828  nmge0  20871  nmmtri  20876  nlmvscnlem2  20929  nrginvrcnlem  20934  nmoix  20971  nmoleub  20973  blcvx  21038  xrsxmet  21049  opnreen  21071  xrge0tsms  21074  icopnfcnv  21177  xrhmeo  21181  lebnumii  21201  pcophtb  21264  pi1grplem  21284  nmoleub2lem  21332  ipcau2  21412  tchcphlem1  21413  ipcau  21416  ipcnlem2  21419  rrxcph  21559  minveclem2  21576  minveclem3b  21578  pjthlem1  21587  pjthlem2  21588  ivthlem3  21600  ivth2  21602  ovolfsf  21618  ovolsslem  21630  ovollb2lem  21634  ovollb2  21635  ovolctb  21636  ovolfiniun  21647  ovolicc1  21662  ovolicc2lem4  21666  ovolicc2  21668  nulmbl2  21682  unmbl  21683  ioombl1lem4  21706  uniioombllem4  21730  uniioombllem6  21732  volivth  21751  vitalilem4  21755  itg1ge0  21828  itg1ge0a  21853  itg1lea  21854  itg1climres  21856  mbfi1fseqlem5  21861  itg2ub  21875  itg2seq  21884  itg2uba  21885  itg2splitlem  21890  itg2split  21891  itg2monolem3  21894  itg2mono  21895  itg2i1fseq2  21898  itg2addlem  21900  iblss  21946  itggt0  21983  dvferm2lem  22122  dvlip  22129  dvivthlem1  22144  dvfsumlem2  22163  dvfsumlem3  22164  ftc1lem4  22175  ply1divmo  22271  ply1remlem  22298  fta1glem2  22302  ig1pdvds  22312  plyeq0lem  22342  plydiveu  22428  fta1lem  22437  vieta1lem2  22441  aaliou3lem2  22473  aaliou3lem8  22475  ulmcn  22528  mtest  22533  itgulm  22537  radcnvlem1  22542  radcnvlt1  22547  dvradcnv  22550  pserdvlem2  22557  abelthlem2  22561  abelthlem6  22565  abelthlem7  22567  abelthlem9  22569  tangtx  22631  sinq12gt0  22633  sineq0  22647  cosordlem  22651  tanord  22658  tanregt0  22659  logrnaddcl  22690  logcj  22719  argregt0  22723  argrege0  22724  argimgt0  22725  argimlt0  22726  logimul  22727  logneg2  22728  logdivlti  22733  divlogrlim  22744  logcnlem3  22753  logcnlem4  22754  dvlog2lem  22761  logtayl  22769  rpcxpcl  22785  cxpsqrtlem  22811  cxpaddle  22854  isosctrlem1  22880  asinlem3a  22929  asinlem3  22930  asinneg  22945  asinsinlem  22950  asinsin  22951  atanlogaddlem  22972  atanlogadd  22973  atanlogsublem  22974  atanlogsub  22975  atantan  22982  atanbndlem  22984  atantayl  22996  leibpi  23001  birthdaylem3  23011  areaf  23019  cxploglim  23035  jensenlem2  23045  jensen  23046  logdiflbnd  23052  harmonicbnd4  23068  fsumharmonic  23069  wilthlem2  23071  ftalem1  23074  ftalem2  23075  ftalem5  23078  basellem6  23087  basellem8  23089  basellem9  23090  chtge0  23114  chtublem  23214  logexprlim  23228  perfectlem1  23232  bcmax  23281  bposlem1  23287  bposlem2  23288  bposlem6  23292  bposlem7  23293  lgsdilem2  23334  lgsqrlem4  23347  lgsquadlem1  23357  2sqlem3  23369  2sqlem8  23375  2sqblem  23380  chebbnd1lem2  23383  chtppilimlem1  23386  chtppilim  23388  chto1ub  23389  vmadivsum  23395  rplogsumlem1  23397  rplogsumlem2  23398  dchrisum0lem1a  23399  rpvmasumlem  23400  dchrisumlem1  23402  dchrisumlem2  23403  dchrvmasumlem2  23411  dchrisum0flblem1  23421  dchrisum0flblem2  23422  dchrisum0lem1b  23428  dchrisum0lem1  23429  dchrisum0lem2a  23430  dchrisum0lem3  23432  dchrisum0  23433  mudivsum  23443  mulogsumlem  23444  mulog2sumlem1  23447  mulog2sumlem2  23448  2vmadivsumlem  23453  chpdifbndlem1  23466  selberg3lem1  23470  selberg4lem1  23473  pntrlog2bndlem1  23490  pntrlog2bndlem2  23491  pntrlog2bndlem3  23492  pntrlog2bndlem4  23493  pntpbnd1a  23498  pntpbnd1  23499  pntpbnd2  23500  pntibndlem2  23504  pntibndlem3  23505  pntlemd  23507  pntlemc  23508  pntlemb  23510  pntlemg  23511  pntlemh  23512  pntlemr  23515  pntlemf  23518  pntlemo  23520  abvcxp  23528  ostth2lem1  23531  padicabv  23543  ostth2lem2  23547  ostth2lem3  23548  ostth2lem4  23549  ostth2  23550  ostth3  23551  legso  23712  krippenlem  23775  mideu  23814  ttgcontlem1  23864  axpaschlem  23919  axcontlem8  23950  umgraex  23999  wwlkextproplem3  24419  clwlkisclwwlk2  24466  clwwlkndivn  24513  clwlkf1clwwlklem1  24522  nvabs  25252  nmooge0  25358  nmoolb  25362  siii  25444  minvecolem2  25467  minvecolem4  25472  minvecolem5  25473  hlipgt0  25506  normge0  25719  normpyc  25739  pjhthlem1  25985  pjige0i  26284  nmoplb  26502  nmfnlb  26519  branmfn  26700  pjssdif2i  26769  stlei  26835  mul2lt0rgt0  27234  xlt2addrd  27246  eliccelico  27256  elicoelioo  27257  bcm1n  27268  omndmul2  27364  archirngz  27395  archiabllem2c  27401  xrge0tsmsd  27438  ofldchr  27467  xrge0iifiso  27553  nexple  27645  gsumesum  27707  esumcst  27711  esumpcvgval  27724  esumcvg  27732  measssd  27826  measunl  27827  sibfof  27922  oddpwdc  27933  eulerpartlemgc  27941  iwrdsplit  27966  ballotlemsgt1  28089  ballotlemsel1i  28091  sgnmul  28121  signsply0  28148  signstfvc  28171  signsvtp  28180  signsvfpn  28182  zetacvg  28197  lgamgulmlem2  28212  lgamgulmlem3  28213  lgamcvg2  28237  subfaclim  28272  erdszelem7  28281  erdszelem8  28282  cvmliftlem2  28371  snmlff  28414  sinccvglem  28513  climlec3  28597  clim2div  28600  ntrivcvgtail  28611  iprodclim2  28695  iprodclim3  28696  faclim  28748  dvdspw  28752  nodense  29026  nobndup  29037  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  itg2addnclem  29643  itg2addnclem3  29645  itg2gt0cn  29647  itggt0cn  29664  ftc1anclem5  29671  ftc1anclem7  29673  ftc1anclem8  29674  fnejoin1  29789  isbnd3  29883  ssbnd  29887  heiborlem8  29917  bfplem2  29922  rrncmslem  29931  rrnequiv  29934  rrntotbnd  29935  eldioph2lem1  30297  lzenom  30307  irrapxlem1  30362  irrapxlem4  30365  irrapxlem5  30366  pell14qrgt0  30399  pell1qrge1  30410  pell1qrgap  30414  pellfundge  30422  pellfundex  30426  pellfund14  30438  rmspecsqrtnq  30446  rmxypos  30489  ltrmynn0  30490  ltrmxnn0  30491  jm2.24nn  30501  jm2.17b  30503  jm2.17c  30504  jm2.24  30505  congadd  30508  congsym  30510  congneg  30511  congid  30513  mzpcong  30514  acongrep  30522  acongeq  30525  jm2.18  30534  jm2.19  30539  jm2.23  30542  jm2.25  30545  jm2.26lem3  30547  jm2.15nn0  30549  jm2.16nn0  30550  jm2.27a  30551  jm2.27c  30553  jm3.1lem1  30563  idomrootle  30757  idomsubgmo  30760  dvdslcm  30804  lcmgcdlem  30812  cncmpmax  30985  fmul01  31130  fmul01lt1lem1  31134  climdivf  31154  stoweidlem1  31301  stoweidlem16  31316  stoweidlem18  31318  stoweidlem24  31324  stoweidlem26  31326  stoweidlem36  31336  stoweidlem38  31338  stoweidlem41  31341  stoweidlem42  31342  stoweidlem44  31344  stoweidlem45  31345  stoweidlem48  31348  stoweidlem62  31362  wallispilem5  31369  stirlinglem1  31374  stirlinglem5  31378  stirlinglem7  31380  stirlinglem8  31381  stirlinglem9  31382  stirlinglem11  31384  fourierdlem74  31481  fourierdlem104  31511  rlimdmafv  31729  2elfz2melfz  31803  usgedgleord  31888  altgsumbcALT  32006  lcv1  33838  lsatcv0eq  33844  lsatcvat3  33849  cvlsupr2  34140  hlatlej2  34172  cvrval4N  34210  cvratlem  34217  atcvr0eq  34222  2atlt  34235  atbtwnex  34244  athgt  34252  1cvrat  34272  ps-1  34273  hlatexch3N  34276  hlatexch4  34277  3atlem2  34280  atcvrlln2  34315  lplnexllnN  34360  4atlem3a  34393  4atlem10b  34401  4atlem11b  34404  4atlem12b  34407  2lplnja  34415  dalemply  34450  dalemsly  34451  dalem1  34455  dalem6  34464  dalem7  34465  dalem-cly  34467  dalem11  34470  dalem12  34471  dalem16  34475  dalem17  34476  dalem38  34506  dalem44  34512  dalem61  34529  lnatexN  34575  lncvrat  34578  lncmp  34579  paddasslem2  34617  dalawlem3  34669  dalawlem6  34672  dalawlem11  34677  lhpmcvr  34819  lhp2atne  34830  lhp2at0ne  34832  lautj  34889  trlval4  34984  cdlemc2  34988  cdlemc5  34991  cdleme3b  35025  cdleme11c  35057  cdleme19a  35099  cdleme20j  35114  cdleme22f  35142  cdleme23c  35147  cdleme26f2ALTN  35160  cdleme26f2  35161  cdleme35fnpq  35245  cdleme48bw  35298  cdlemg10a  35436  cdlemg11b  35438  cdlemg17g  35463  cdlemg18c  35476  cdlemi1  35614  cdlemk52  35750  dia2dimlem1  35861  dihord1  36015  dihjatcclem4  36218
  Copyright terms: Public domain W3C validator