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

Theorem breqtrrd 4460
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 2449 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4458 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381   class class class wbr 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435
This theorem is referenced by:  marypha1lem  7892  marypha2  7898  unxpwdom  8015  uncdadom  8551  cdacomen  8561  cdaassen  8562  xpcdaen  8563  onacda  8577  infcdaabs  8586  cfss  8645  tskuni  9161  ltexnq  9353  xrmax1  11382  xrmax2  11383  max1ALT  11393  qbtwnxr  11405  xleadd1a  11451  xlt2add  11458  xlesubadd  11461  xmulgt0  11481  xlemul1a  11486  xov1plusxeqvd  11672  uzsubsubfz  11713  fzctr  11792  flflp1  11920  ceilge  11949  modge0  11981  modlt  11982  modid  11996  modaddmodup  12026  sermono  12115  seqf1olem1  12122  seqf1olem2  12123  leexp1a  12200  sqgt0  12212  sqge0  12220  nnlesq  12247  expnbnd  12271  expmulnbnd  12274  discr1  12278  facwordi  12343  faclbnd5  12352  hashdom  12423  brfi1uzind  12508  ccatws1n0  12612  swrds2  12859  cjmulge0  12955  resqrtcl  13063  absge0  13096  sqreulem  13168  amgm2  13178  rlimdm  13350  rlimge0  13380  reccn2  13395  climle  13438  climserle  13461  isercoll2  13467  iseraltlem1  13480  iseralt  13483  isumclim2  13549  isumclim3  13550  isumge0  13557  fsumless  13586  cvgcmp  13606  cvgcmpce  13608  abscvgcvg  13609  isumsup2  13634  isumltss  13636  climcndslem1  13637  climcnds  13639  supcvg  13643  harmonic  13646  expcnv  13651  explecnv  13652  cvgrat  13668  mertenslem1  13669  mertenslem2  13670  efcvg  13695  ege2le3  13700  efaddlem  13703  eftlub  13718  effsumlt  13720  tanhlt1  13769  ef01bndlem  13793  sin02gt0  13801  rpnnen2lem4  13825  ruclem2  13839  ruclem3  13840  ruclem9  13845  iddvdsexp  13881  dvdsadd  13898  dvdsfac  13915  dvdsmod  13917  3dvds  13924  divalglem1  13926  bitsfzo  13959  bitsmod  13960  bitscmp  13962  bitsinv1lem  13965  sadcaddlem  13981  sadadd3  13985  sadaddlem  13990  dvdssqim  14065  dvdsmulgcd  14066  nn0seqcvgd  14073  sqnprm  14113  mulgcddvds  14119  qredeq  14121  isprm6  14124  nonsq  14166  hashdvds  14179  prmdiv  14189  odzdvds  14196  omoe  14210  pythagtriplem4  14217  pcpre1  14240  pcdvdsb  14266  pcz  14278  pcprmpw2  14279  pcaddlem  14281  pcadd  14282  pcadd2  14283  pcmpt  14285  pcmptdvds  14287  fldivp1  14290  pcfaclem  14291  pockthlem  14297  prmreclem1  14308  prmreclem3  14310  prmreclem5  14312  prmreclem6  14313  4sqlem6  14335  4sqlem8  14337  4sqlem11  14347  4sqlem12  14348  4sqlem14  14350  4sqlem16  14352  vdwlem3  14375  vdwlem9  14381  vdwlem10  14382  vdwlem12  14384  ramub1lem2  14419  invfuc  15214  ple1  15545  eqgen  16125  lagsubg  16134  pgpfi  16496  sylow2alem2  16509  sylow2a  16510  sylow3lem4  16521  efgsrel  16623  odadd1  16725  odadd2  16726  gexex  16730  lt6abl  16768  dprd2d2  16964  dmdprdpr  16969  ablfacrp2  16989  ablfac1c  16993  pgpfaclem1  17003  ablfac2  17011  dvdsrmul1  17173  unitmulclb  17185  subrguss  17315  abvres  17359  ply1coefsupp  18207  evl1gsumadd  18265  znfld  18469  znunit  18472  frlmisfrlm  18753  matgsum  18809  pm2mpcl  19168  psmetxrge0  20687  isxmet2d  20700  mettri  20725  xmettri3  20726  mettri3  20727  xmetrtri2  20729  prdsxmetlem  20741  imasdsf1olem  20746  xblss2ps  20774  blss2ps  20776  blss2  20777  blssps  20797  blss  20798  prdsbl  20864  dscmet  20963  nmge0  21006  nmmtri  21011  nlmvscnlem2  21064  nrginvrcnlem  21069  nmoix  21106  nmoleub  21108  blcvx  21173  xrsxmet  21184  opnreen  21206  xrge0tsms  21209  icopnfcnv  21312  xrhmeo  21316  lebnumii  21336  pcophtb  21399  pi1grplem  21419  nmoleub2lem  21467  ipcau2  21547  tchcphlem1  21548  ipcau  21551  ipcnlem2  21554  rrxcph  21694  minveclem2  21711  minveclem3b  21713  pjthlem1  21722  pjthlem2  21723  ivthlem3  21735  ivth2  21737  ovolfsf  21753  ovolsslem  21765  ovollb2lem  21769  ovollb2  21770  ovolctb  21771  ovolfiniun  21782  ovolicc1  21797  ovolicc2lem4  21801  ovolicc2  21803  nulmbl2  21817  unmbl  21818  ioombl1lem4  21841  uniioombllem4  21865  uniioombllem6  21867  volivth  21886  vitalilem4  21890  itg1ge0  21963  itg1ge0a  21988  itg1lea  21989  itg1climres  21991  mbfi1fseqlem5  21996  itg2ub  22010  itg2seq  22019  itg2uba  22020  itg2splitlem  22025  itg2split  22026  itg2monolem3  22029  itg2mono  22030  itg2i1fseq2  22033  itg2addlem  22035  iblss  22081  itggt0  22118  dvferm2lem  22257  dvlip  22264  dvivthlem1  22279  dvfsumlem2  22298  dvfsumlem3  22299  ftc1lem4  22310  ply1divmo  22406  ply1remlem  22433  fta1glem2  22437  ig1pdvds  22447  plyeq0lem  22477  plydiveu  22563  fta1lem  22572  vieta1lem2  22576  aaliou3lem2  22608  aaliou3lem8  22610  ulmcn  22663  mtest  22668  itgulm  22672  radcnvlem1  22677  radcnvlt1  22682  dvradcnv  22685  pserdvlem2  22692  abelthlem2  22696  abelthlem6  22700  abelthlem7  22702  abelthlem9  22704  tangtx  22767  sinq12gt0  22769  sineq0  22783  cosordlem  22787  tanord  22794  tanregt0  22795  logrnaddcl  22831  logcj  22860  argregt0  22864  argrege0  22865  argimgt0  22866  argimlt0  22867  logimul  22868  logneg2  22869  logdivlti  22874  divlogrlim  22885  logcnlem3  22894  logcnlem4  22895  dvlog2lem  22902  logtayl  22910  rpcxpcl  22926  cxpsqrtlem  22952  cxpaddle  22995  isosctrlem1  23021  asinlem3a  23070  asinlem3  23071  asinneg  23086  asinsinlem  23091  asinsin  23092  atanlogaddlem  23113  atanlogadd  23114  atanlogsublem  23115  atanlogsub  23116  atantan  23123  atanbndlem  23125  atantayl  23137  leibpi  23142  birthdaylem3  23152  areaf  23160  cxploglim  23176  jensenlem2  23186  jensen  23187  logdiflbnd  23193  harmonicbnd4  23209  fsumharmonic  23210  wilthlem2  23212  ftalem1  23215  ftalem2  23216  ftalem5  23219  basellem6  23228  basellem8  23230  basellem9  23231  chtge0  23255  chtublem  23355  logexprlim  23369  perfectlem1  23373  bcmax  23422  bposlem1  23428  bposlem2  23429  bposlem6  23433  bposlem7  23434  lgsdilem2  23475  lgsqrlem4  23488  lgsquadlem1  23498  2sqlem3  23510  2sqlem8  23516  2sqblem  23521  chebbnd1lem2  23524  chtppilimlem1  23527  chtppilim  23529  chto1ub  23530  vmadivsum  23536  rplogsumlem1  23538  rplogsumlem2  23539  dchrisum0lem1a  23540  rpvmasumlem  23541  dchrisumlem1  23543  dchrisumlem2  23544  dchrvmasumlem2  23552  dchrisum0flblem1  23562  dchrisum0flblem2  23563  dchrisum0lem1b  23569  dchrisum0lem1  23570  dchrisum0lem2a  23571  dchrisum0lem3  23573  dchrisum0  23574  mudivsum  23584  mulogsumlem  23585  mulog2sumlem1  23588  mulog2sumlem2  23589  2vmadivsumlem  23594  chpdifbndlem1  23607  selberg3lem1  23611  selberg4lem1  23614  pntrlog2bndlem1  23631  pntrlog2bndlem2  23632  pntrlog2bndlem3  23633  pntrlog2bndlem4  23634  pntpbnd1a  23639  pntpbnd1  23640  pntpbnd2  23641  pntibndlem2  23645  pntibndlem3  23646  pntlemd  23648  pntlemc  23649  pntlemb  23651  pntlemg  23652  pntlemh  23653  pntlemr  23656  pntlemf  23659  pntlemo  23661  abvcxp  23669  ostth2lem1  23672  padicabv  23684  ostth2lem2  23688  ostth2lem3  23689  ostth2lem4  23690  ostth2  23691  ostth3  23692  legso  23854  krippenlem  23936  midex  23980  ttgcontlem1  24057  axpaschlem  24112  axcontlem8  24143  umgraex  24192  wwlkextproplem3  24612  clwlkisclwwlk2  24659  clwwlkndivn  24706  clwlkf1clwwlklem1  24715  ex-ind-dvds  25039  nvabs  25445  nmooge0  25551  nmoolb  25555  siii  25637  minvecolem2  25660  minvecolem4  25665  minvecolem5  25666  hlipgt0  25699  normge0  25912  normpyc  25932  pjhthlem1  26178  pjige0i  26477  nmoplb  26695  nmfnlb  26712  branmfn  26893  pjssdif2i  26962  stlei  27028  mul2lt0rgt0  27435  xlt2addrd  27447  eliccelico  27457  elicoelioo  27458  bcm1n  27469  2sqmod  27506  omndmul2  27572  archirngz  27603  archiabllem2c  27609  xrge0tsmsd  27645  ofldchr  27674  locfinreflem  27713  xrge0iifiso  27787  nexple  27875  gsumesum  27937  esumcst  27941  esumpcvgval  27954  esumcvg  27962  measssd  28056  measunl  28057  sibfof  28152  oddpwdc  28163  eulerpartlemgc  28171  iwrdsplit  28196  ballotlemsgt1  28319  ballotlemsel1i  28321  sgnmul  28351  signsply0  28378  signstfvc  28401  signsvtp  28410  signsvfpn  28412  zetacvg  28427  lgamgulmlem2  28442  lgamgulmlem3  28443  lgamcvg2  28467  subfaclim  28502  erdszelem7  28511  erdszelem8  28512  cvmliftlem2  28601  snmlff  28644  sinccvglem  28908  climlec3  28992  clim2div  28995  ntrivcvgtail  29006  iprodclim2  29090  iprodclim3  29091  faclim  29143  dvdspw  29147  nodense  29421  nobndup  29432  mblfinlem2  30024  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  itg2addnclem  30038  itg2addnclem3  30040  itg2gt0cn  30042  itggt0cn  30059  ftc1anclem5  30066  ftc1anclem7  30068  ftc1anclem8  30069  fnejoin1  30158  isbnd3  30252  ssbnd  30256  heiborlem8  30286  bfplem2  30291  rrncmslem  30300  rrnequiv  30303  rrntotbnd  30304  eldioph2lem1  30665  lzenom  30675  irrapxlem1  30730  irrapxlem4  30733  irrapxlem5  30734  pell14qrgt0  30767  pell1qrge1  30778  pell1qrgap  30782  pellfundge  30790  pellfundex  30794  pellfund14  30806  rmspecsqrtnq  30814  rmxypos  30857  ltrmynn0  30858  ltrmxnn0  30859  jm2.24nn  30869  jm2.17b  30871  jm2.17c  30872  jm2.24  30873  congadd  30876  congsym  30878  congneg  30879  congid  30881  mzpcong  30882  acongrep  30890  acongeq  30893  jm2.18  30902  jm2.19  30907  jm2.23  30910  jm2.25  30913  jm2.26lem3  30915  jm2.15nn0  30917  jm2.16nn0  30918  jm2.27a  30919  jm2.27c  30921  jm3.1lem1  30931  idomrootle  31125  idomsubgmo  31128  dvgrat  31166  radcnvrat  31168  dvdslcm  31177  lcmgcdlem  31185  cncmpmax  31358  zltlesub  31417  lt2addmuld  31422  fmul01  31502  fmul01lt1lem1  31506  climdivf  31526  sumnnodd  31544  dvdivbd  31624  volge0  31650  stoweidlem1  31672  stoweidlem16  31687  stoweidlem18  31689  stoweidlem24  31695  stoweidlem26  31697  stoweidlem36  31707  stoweidlem38  31709  stoweidlem41  31712  stoweidlem42  31713  stoweidlem44  31715  stoweidlem45  31716  stoweidlem48  31719  stoweidlem62  31733  wallispilem5  31740  stirlinglem1  31745  stirlinglem5  31749  stirlinglem7  31751  stirlinglem8  31752  stirlinglem9  31753  stirlinglem11  31755  fourierdlem4  31782  fourierdlem10  31788  fourierdlem37  31815  fourierdlem47  31825  fourierdlem72  31850  fourierdlem74  31852  fourierdlem79  31857  fourierdlem82  31860  fourierdlem89  31867  fourierdlem91  31869  fourierdlem93  31871  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  rlimdmafv  32100  2elfz2melfz  32172  usgedgleord  32257  cznnring  32471  rhmsubcrngc  32569  altgsumbcALT  32670  lcv1  34489  lsatcv0eq  34495  lsatcvat3  34500  cvlsupr2  34791  hlatlej2  34823  cvrval4N  34861  cvratlem  34868  atcvr0eq  34873  2atlt  34886  atbtwnex  34895  athgt  34903  1cvrat  34923  ps-1  34924  hlatexch3N  34927  hlatexch4  34928  3atlem2  34931  atcvrlln2  34966  lplnexllnN  35011  4atlem3a  35044  4atlem10b  35052  4atlem11b  35055  4atlem12b  35058  2lplnja  35066  dalemply  35101  dalemsly  35102  dalem1  35106  dalem6  35115  dalem7  35116  dalem-cly  35118  dalem11  35121  dalem12  35122  dalem16  35126  dalem17  35127  dalem38  35157  dalem44  35163  dalem61  35180  lnatexN  35226  lncvrat  35229  lncmp  35230  paddasslem2  35268  dalawlem3  35320  dalawlem6  35323  dalawlem11  35328  lhpmcvr  35470  lhp2atne  35481  lhp2at0ne  35483  lautj  35540  trlval4  35636  cdlemc2  35640  cdlemc5  35643  cdleme3b  35677  cdleme11c  35709  cdleme19a  35752  cdleme20j  35767  cdleme22f  35795  cdleme23c  35800  cdleme26f2ALTN  35813  cdleme26f2  35814  cdleme35fnpq  35898  cdleme48bw  35951  cdlemg10a  36089  cdlemg11b  36091  cdlemg17g  36116  cdlemg18c  36129  cdlemi1  36267  cdlemk52  36403  dia2dimlem1  36514  dihord1  36668  dihjatcclem4  36871  inductionexd  37620  imo72b2  37645
  Copyright terms: Public domain W3C validator