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

Theorem breqtrrd 4416
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 2459 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4414 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   class class class wbr 4390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391
This theorem is referenced by:  marypha1lem  7784  marypha2  7790  unxpwdom  7905  uncdadom  8441  cdacomen  8451  cdaassen  8452  xpcdaen  8453  onacda  8467  infcdaabs  8476  cfss  8535  tskuni  9051  ltexnq  9245  xrmax1  11248  xrmax2  11249  max1ALT  11259  qbtwnxr  11271  xleadd1a  11317  xlt2add  11324  xlesubadd  11327  xmulgt0  11347  xlemul1a  11352  xov1plusxeqvd  11532  uzsubsubfz  11572  fzctr  11630  ceilge  11786  modge0  11818  modlt  11819  modid  11833  modaddmodup  11863  sermono  11939  seqf1olem1  11946  seqf1olem2  11947  leexp1a  12023  sqgt0  12035  sqge0  12043  nnlesq  12070  expnbnd  12094  expmulnbnd  12097  discr1  12101  facwordi  12166  faclbnd5  12175  hashdom  12244  brfi1uzind  12321  ccatws1n0  12412  swrds2  12647  cjmulge0  12737  resqrcl  12845  absge0  12878  sqreulem  12949  amgm2  12959  rlimdm  13131  rlimge0  13161  reccn2  13176  climle  13219  climserle  13242  isercoll2  13248  iseraltlem1  13261  iseralt  13264  isumclim2  13327  isumclim3  13328  isumge0  13335  fsumless  13361  cvgcmp  13381  cvgcmpce  13383  abscvgcvg  13384  isumsup2  13411  isumltss  13413  climcndslem1  13414  climcnds  13416  supcvg  13420  harmonic  13423  expcnv  13428  explecnv  13429  cvgrat  13445  mertenslem1  13446  mertenslem2  13447  efcvg  13472  ege2le3  13477  efaddlem  13480  eftlub  13495  effsumlt  13497  tanhlt1  13546  ef01bndlem  13570  sin02gt0  13578  rpnnen2lem4  13602  ruclem2  13616  ruclem3  13617  ruclem9  13622  iddvdsexp  13658  dvdsadd  13673  dvdsfac  13690  dvdsmod  13692  3dvds  13698  divalglem1  13700  bitsfzo  13733  bitsmod  13734  bitscmp  13736  bitsinv1lem  13739  sadcaddlem  13755  sadadd3  13759  sadaddlem  13764  dvdssqim  13839  dvdsmulgcd  13840  nn0seqcvgd  13847  sqnprm  13886  mulgcddvds  13892  qredeq  13894  isprm6  13897  nonsq  13939  hashdvds  13952  prmdiv  13962  odzdvds  13969  omoe  13981  pythagtriplem4  13988  pcpre1  14011  pcdvdsb  14037  pcz  14049  pcprmpw2  14050  pcaddlem  14052  pcadd  14053  pcadd2  14054  pcmpt  14056  pcmptdvds  14058  fldivp1  14061  pcfaclem  14062  pockthlem  14068  prmreclem1  14079  prmreclem3  14081  prmreclem5  14083  prmreclem6  14084  4sqlem6  14106  4sqlem8  14108  4sqlem11  14118  4sqlem12  14119  4sqlem14  14121  4sqlem16  14123  vdwlem3  14146  vdwlem9  14152  vdwlem10  14153  vdwlem12  14155  ramub1lem2  14190  invfuc  14986  ple1  15316  eqgen  15836  lagsubg  15845  pgpfi  16208  sylow2alem2  16221  sylow2a  16222  sylow3lem4  16233  efgsrel  16335  odadd1  16434  odadd2  16435  gexex  16439  lt6abl  16475  dprd2d2  16648  dmdprdpr  16653  ablfacrp2  16673  ablfac1c  16677  pgpfaclem1  16687  ablfac2  16695  dvdsrmul1  16851  unitmulclb  16863  subrguss  16986  abvres  17030  ply1coefsupp  17854  evl1gsumadd  17901  znfld  18102  znunit  18105  frlmisfrlm  18386  psmetxrge0  20005  isxmet2d  20018  mettri  20043  xmettri3  20044  mettri3  20045  xmetrtri2  20047  prdsxmetlem  20059  imasdsf1olem  20064  xblss2ps  20092  blss2ps  20094  blss2  20095  blssps  20115  blss  20116  prdsbl  20182  dscmet  20281  nmge0  20324  nmmtri  20329  nlmvscnlem2  20382  nrginvrcnlem  20387  nmoix  20424  nmoleub  20426  blcvx  20491  xrsxmet  20502  opnreen  20524  xrge0tsms  20527  icopnfcnv  20630  xrhmeo  20634  lebnumii  20654  pcophtb  20717  pi1grplem  20737  nmoleub2lem  20785  ipcau2  20865  tchcphlem1  20866  ipcau  20869  ipcnlem2  20872  rrxcph  21012  minveclem2  21029  minveclem3b  21031  pjthlem1  21040  pjthlem2  21041  ivthlem3  21053  ivth2  21055  ovolfsf  21071  ovolsslem  21083  ovollb2lem  21087  ovollb2  21088  ovolctb  21089  ovolfiniun  21100  ovolicc1  21115  ovolicc2lem4  21119  ovolicc2  21121  nulmbl2  21134  unmbl  21135  ioombl1lem4  21158  uniioombllem4  21182  uniioombllem6  21184  volivth  21203  vitalilem4  21207  itg1ge0  21280  itg1ge0a  21305  itg1lea  21306  itg1climres  21308  mbfi1fseqlem5  21313  itg2ub  21327  itg2seq  21336  itg2uba  21337  itg2splitlem  21342  itg2split  21343  itg2monolem3  21346  itg2mono  21347  itg2i1fseq2  21350  itg2addlem  21352  iblss  21398  itggt0  21435  dvferm2lem  21574  dvlip  21581  dvivthlem1  21596  dvfsumlem2  21615  dvfsumlem3  21616  ftc1lem4  21627  ply1divmo  21723  ply1remlem  21750  fta1glem2  21754  ig1pdvds  21764  plyeq0lem  21794  plydiveu  21880  fta1lem  21889  vieta1lem2  21893  aaliou3lem2  21925  aaliou3lem8  21927  ulmcn  21980  mtest  21985  itgulm  21989  radcnvlem1  21994  radcnvlt1  21999  dvradcnv  22002  pserdvlem2  22009  abelthlem2  22013  abelthlem6  22017  abelthlem7  22019  abelthlem9  22021  tangtx  22083  sinq12gt0  22085  sineq0  22099  cosordlem  22103  tanord  22110  tanregt0  22111  logrnaddcl  22142  logcj  22171  argregt0  22175  argrege0  22176  argimgt0  22177  argimlt0  22178  logimul  22179  logneg2  22180  logdivlti  22185  divlogrlim  22196  logcnlem3  22205  logcnlem4  22206  dvlog2lem  22213  logtayl  22221  rpcxpcl  22237  cxpsqrlem  22263  cxpaddle  22306  isosctrlem1  22332  asinlem3a  22381  asinlem3  22382  asinneg  22397  asinsinlem  22402  asinsin  22403  atanlogaddlem  22424  atanlogadd  22425  atanlogsublem  22426  atanlogsub  22427  atantan  22434  atanbndlem  22436  atantayl  22448  leibpi  22453  birthdaylem3  22463  areaf  22471  cxploglim  22487  jensenlem2  22497  jensen  22498  logdiflbnd  22504  harmonicbnd4  22520  fsumharmonic  22521  wilthlem2  22523  ftalem1  22526  ftalem2  22527  ftalem5  22530  basellem6  22539  basellem8  22541  basellem9  22542  chtge0  22566  chtublem  22666  logexprlim  22680  perfectlem1  22684  bcmax  22733  bposlem1  22739  bposlem2  22740  bposlem6  22744  bposlem7  22745  lgsdilem2  22786  lgsqrlem4  22799  lgsquadlem1  22809  2sqlem3  22821  2sqlem8  22827  2sqblem  22832  chebbnd1lem2  22835  chtppilimlem1  22838  chtppilim  22840  chto1ub  22841  vmadivsum  22847  rplogsumlem1  22849  rplogsumlem2  22850  dchrisum0lem1a  22851  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem2  22855  dchrvmasumlem2  22863  dchrisum0flblem1  22873  dchrisum0flblem2  22874  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem3  22884  dchrisum0  22885  mudivsum  22895  mulogsumlem  22896  mulog2sumlem1  22899  mulog2sumlem2  22900  2vmadivsumlem  22905  chpdifbndlem1  22918  selberg3lem1  22922  selberg4lem1  22925  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntibndlem3  22957  pntlemd  22959  pntlemc  22960  pntlemb  22962  pntlemg  22963  pntlemh  22964  pntlemr  22967  pntlemf  22970  pntlemo  22972  abvcxp  22980  ostth2lem1  22983  padicabv  22995  ostth2lem2  22999  ostth2lem3  23000  ostth2lem4  23001  ostth2  23002  ostth3  23003  krippenlem  23210  mideu  23245  ttgcontlem1  23266  axpaschlem  23321  axcontlem8  23352  umgraex  23392  nvabs  24196  nmooge0  24302  nmoolb  24306  siii  24388  minvecolem2  24411  minvecolem4  24416  minvecolem5  24417  hlipgt0  24450  normge0  24663  normpyc  24683  pjhthlem1  24929  pjige0i  25228  nmoplb  25446  nmfnlb  25463  branmfn  25644  pjssdif2i  25713  stlei  25779  mul2lt0rgt0  26173  xlt2addrd  26185  eliccelico  26201  elicoelioo  26202  bcm1n  26213  omndmul2  26309  archirngz  26340  archiabllem2c  26346  xrge0tsmsd  26387  ofldchr  26416  xrge0iifiso  26499  nexple  26582  gsumesum  26644  esumcst  26648  esumpcvgval  26661  esumcvg  26669  measssd  26763  measunl  26764  sibfof  26860  oddpwdc  26871  eulerpartlemgc  26879  iwrdsplit  26904  ballotlemsgt1  27027  ballotlemsel1i  27029  sgnmul  27059  signsply0  27086  signstfvc  27109  signsvtp  27118  signsvfpn  27120  zetacvg  27135  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamcvg2  27175  subfaclim  27210  erdszelem7  27219  erdszelem8  27220  cvmliftlem2  27309  snmlff  27352  sinccvglem  27451  climlec3  27535  clim2div  27538  ntrivcvgtail  27549  iprodclim2  27633  iprodclim3  27634  faclim  27686  dvdspw  27690  nodense  27964  nobndup  27975  lxflflp1  28559  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  itg2addnclem  28581  itg2addnclem3  28583  itg2gt0cn  28585  itggt0cn  28602  ftc1anclem5  28609  ftc1anclem7  28611  ftc1anclem8  28612  fnejoin1  28727  isbnd3  28821  ssbnd  28825  heiborlem8  28855  bfplem2  28860  rrncmslem  28869  rrnequiv  28872  rrntotbnd  28873  eldioph2lem1  29236  lzenom  29246  irrapxlem1  29301  irrapxlem4  29304  irrapxlem5  29305  pell14qrgt0  29338  pell1qrge1  29349  pell1qrgap  29353  pellfundge  29361  pellfundex  29365  pellfund14  29377  rmspecsqrnq  29385  rmxypos  29428  ltrmynn0  29429  ltrmxnn0  29430  jm2.24nn  29440  jm2.17b  29442  jm2.17c  29443  jm2.24  29444  congadd  29447  congsym  29449  congneg  29450  congid  29452  mzpcong  29453  acongrep  29461  acongeq  29464  jm2.18  29475  jm2.19  29480  jm2.23  29483  jm2.25  29486  jm2.26lem3  29488  jm2.15nn0  29490  jm2.16nn0  29491  jm2.27a  29492  jm2.27c  29494  jm3.1lem1  29504  idomrootle  29698  idomsubgmo  29701  cncmpmax  29892  fmul01  29899  fmul01lt1lem1  29903  climdivf  29923  stoweidlem1  29934  stoweidlem16  29949  stoweidlem18  29951  stoweidlem24  29957  stoweidlem26  29959  stoweidlem36  29969  stoweidlem38  29971  stoweidlem41  29974  stoweidlem42  29975  stoweidlem44  29977  stoweidlem45  29978  stoweidlem48  29981  stoweidlem62  29995  wallispilem5  30002  stirlinglem1  30007  stirlinglem5  30011  stirlinglem7  30013  stirlinglem8  30014  stirlinglem9  30015  stirlinglem11  30017  rlimdmafv  30221  2elfz2melfz  30340  clwlkisclwwlk2  30590  clwwlkndivn  30649  clwlkf1clwwlklem1  30657  wwlkextproplem3  30700  altgsumbcALT  30888  matgsum  31015  lcv1  32992  lsatcv0eq  32998  lsatcvat3  33003  cvlsupr2  33294  hlatlej2  33326  cvrval4N  33364  cvratlem  33371  atcvr0eq  33376  2atlt  33389  atbtwnex  33398  athgt  33406  1cvrat  33426  ps-1  33427  hlatexch3N  33430  hlatexch4  33431  3atlem2  33434  atcvrlln2  33469  lplnexllnN  33514  4atlem3a  33547  4atlem10b  33555  4atlem11b  33558  4atlem12b  33561  2lplnja  33569  dalemply  33604  dalemsly  33605  dalem1  33609  dalem6  33618  dalem7  33619  dalem-cly  33621  dalem11  33624  dalem12  33625  dalem16  33629  dalem17  33630  dalem38  33660  dalem44  33666  dalem61  33683  lnatexN  33729  lncvrat  33732  lncmp  33733  paddasslem2  33771  dalawlem3  33823  dalawlem6  33826  dalawlem11  33831  lhpmcvr  33973  lhp2atne  33984  lhp2at0ne  33986  lautj  34043  trlval4  34138  cdlemc2  34142  cdlemc5  34145  cdleme3b  34179  cdleme11c  34211  cdleme19a  34253  cdleme20j  34268  cdleme22f  34296  cdleme23c  34301  cdleme26f2ALTN  34314  cdleme26f2  34315  cdleme35fnpq  34399  cdleme48bw  34452  cdlemg10a  34590  cdlemg11b  34592  cdlemg17g  34617  cdlemg18c  34630  cdlemi1  34768  cdlemk52  34904  dia2dimlem1  35015  dihord1  35169  dihjatcclem4  35372
  Copyright terms: Public domain W3C validator