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

Theorem breqtrrd 4306
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 2438 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4304 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  marypha1lem  7671  marypha2  7677  unxpwdom  7792  uncdadom  8328  cdacomen  8338  cdaassen  8339  xpcdaen  8340  onacda  8354  infcdaabs  8363  cfss  8422  tskuni  8937  ltexnq  9131  xrmax1  11134  xrmax2  11135  max1ALT  11145  qbtwnxr  11157  xleadd1a  11203  xlt2add  11210  xlesubadd  11213  xmulgt0  11233  xlemul1a  11238  xov1plusxeqvd  11417  uzsubsubfz  11457  fzctr  11512  ceilge  11668  modge0  11700  modlt  11701  modid  11715  modaddmodup  11745  sermono  11821  seqf1olem1  11828  seqf1olem2  11829  leexp1a  11905  sqgt0  11917  sqge0  11925  nnlesq  11952  expnbnd  11976  expmulnbnd  11979  discr1  11983  facwordi  12048  faclbnd5  12057  hashdom  12125  brfi1uzind  12202  ccatws1n0  12293  swrds2  12528  cjmulge0  12618  resqrcl  12726  absge0  12759  sqreulem  12830  amgm2  12840  rlimdm  13012  rlimge0  13042  reccn2  13057  climle  13100  climserle  13123  isercoll2  13129  iseraltlem1  13142  iseralt  13145  isumclim2  13208  isumclim3  13209  isumge0  13216  fsumless  13241  cvgcmp  13261  cvgcmpce  13263  abscvgcvg  13264  isumsup2  13291  isumltss  13293  climcndslem1  13294  climcnds  13296  supcvg  13300  harmonic  13303  expcnv  13308  explecnv  13309  cvgrat  13325  mertenslem1  13326  mertenslem2  13327  efcvg  13352  ege2le3  13357  efaddlem  13360  eftlub  13375  effsumlt  13377  tanhlt1  13426  ef01bndlem  13450  sin02gt0  13458  rpnnen2lem4  13482  ruclem2  13496  ruclem3  13497  ruclem9  13502  iddvdsexp  13538  dvdsadd  13553  dvdsfac  13570  dvdsmod  13572  3dvds  13578  divalglem1  13580  bitsfzo  13613  bitsmod  13614  bitscmp  13616  bitsinv1lem  13619  sadcaddlem  13635  sadadd3  13639  sadaddlem  13644  dvdssqim  13719  dvdsmulgcd  13720  nn0seqcvgd  13727  sqnprm  13766  mulgcddvds  13772  qredeq  13774  isprm6  13777  nonsq  13819  hashdvds  13832  prmdiv  13842  odzdvds  13849  omoe  13861  pythagtriplem4  13868  pcpre1  13891  pcdvdsb  13917  pcz  13929  pcprmpw2  13930  pcaddlem  13932  pcadd  13933  pcadd2  13934  pcmpt  13936  pcmptdvds  13938  fldivp1  13941  pcfaclem  13942  pockthlem  13948  prmreclem1  13959  prmreclem3  13961  prmreclem5  13963  prmreclem6  13964  4sqlem6  13986  4sqlem8  13988  4sqlem11  13998  4sqlem12  13999  4sqlem14  14001  4sqlem16  14003  vdwlem3  14026  vdwlem9  14032  vdwlem10  14033  vdwlem12  14035  ramub1lem2  14070  invfuc  14866  ple1  15196  eqgen  15713  lagsubg  15722  pgpfi  16083  sylow2alem2  16096  sylow2a  16097  sylow3lem4  16108  efgsrel  16210  odadd1  16309  odadd2  16310  gexex  16314  lt6abl  16350  dprd2d2  16516  dmdprdpr  16521  ablfacrp2  16541  ablfac1c  16545  pgpfaclem1  16555  ablfac2  16563  dvdsrmul1  16678  unitmulclb  16690  subrguss  16803  abvres  16847  znfld  17834  znunit  17837  frlmisfrlm  18118  psmetxrge0  19730  isxmet2d  19743  mettri  19768  xmettri3  19769  mettri3  19770  xmetrtri2  19772  prdsxmetlem  19784  imasdsf1olem  19789  xblss2ps  19817  blss2ps  19819  blss2  19820  blssps  19840  blss  19841  prdsbl  19907  dscmet  20006  nmge0  20049  nmmtri  20054  nlmvscnlem2  20107  nrginvrcnlem  20112  nmoix  20149  nmoleub  20151  blcvx  20216  xrsxmet  20227  opnreen  20249  xrge0tsms  20252  icopnfcnv  20355  xrhmeo  20359  lebnumii  20379  pcophtb  20442  pi1grplem  20462  nmoleub2lem  20510  ipcau2  20590  tchcphlem1  20591  ipcau  20594  ipcnlem2  20597  rrxcph  20737  minveclem2  20754  minveclem3b  20756  pjthlem1  20765  pjthlem2  20766  ivthlem3  20778  ivth2  20780  ovolfsf  20796  ovolsslem  20808  ovollb2lem  20812  ovollb2  20813  ovolctb  20814  ovolfiniun  20825  ovolicc1  20840  ovolicc2lem4  20844  ovolicc2  20846  nulmbl2  20859  unmbl  20860  ioombl1lem4  20883  uniioombllem4  20907  uniioombllem6  20909  volivth  20928  vitalilem4  20932  itg1ge0  21005  itg1ge0a  21030  itg1lea  21031  itg1climres  21033  mbfi1fseqlem5  21038  itg2ub  21052  itg2seq  21061  itg2uba  21062  itg2splitlem  21067  itg2split  21068  itg2monolem3  21071  itg2mono  21072  itg2i1fseq2  21075  itg2addlem  21077  iblss  21123  itggt0  21160  dvferm2lem  21299  dvlip  21306  dvivthlem1  21321  dvfsumlem2  21340  dvfsumlem3  21341  ftc1lem4  21352  ply1divmo  21491  ply1remlem  21518  fta1glem2  21522  ig1pdvds  21532  plyeq0lem  21562  plydiveu  21648  fta1lem  21657  vieta1lem2  21661  aaliou3lem2  21693  aaliou3lem8  21695  ulmcn  21748  mtest  21753  itgulm  21757  radcnvlem1  21762  radcnvlt1  21767  dvradcnv  21770  pserdvlem2  21777  abelthlem2  21781  abelthlem6  21785  abelthlem7  21787  abelthlem9  21789  tangtx  21851  sinq12gt0  21853  sineq0  21867  cosordlem  21871  tanord  21878  tanregt0  21879  logrnaddcl  21910  logcj  21939  argregt0  21943  argrege0  21944  argimgt0  21945  argimlt0  21946  logimul  21947  logneg2  21948  logdivlti  21953  divlogrlim  21964  logcnlem3  21973  logcnlem4  21974  dvlog2lem  21981  logtayl  21989  rpcxpcl  22005  cxpsqrlem  22031  cxpaddle  22074  isosctrlem1  22100  asinlem3a  22149  asinlem3  22150  asinneg  22165  asinsinlem  22170  asinsin  22171  atanlogaddlem  22192  atanlogadd  22193  atanlogsublem  22194  atanlogsub  22195  atantan  22202  atanbndlem  22204  atantayl  22216  leibpi  22221  birthdaylem3  22231  areaf  22239  cxploglim  22255  jensenlem2  22265  jensen  22266  logdiflbnd  22272  harmonicbnd4  22288  fsumharmonic  22289  wilthlem2  22291  ftalem1  22294  ftalem2  22295  ftalem5  22298  basellem6  22307  basellem8  22309  basellem9  22310  chtge0  22334  chtublem  22434  logexprlim  22448  perfectlem1  22452  bcmax  22501  bposlem1  22507  bposlem2  22508  bposlem6  22512  bposlem7  22513  lgsdilem2  22554  lgsqrlem4  22567  lgsquadlem1  22577  2sqlem3  22589  2sqlem8  22595  2sqblem  22600  chebbnd1lem2  22603  chtppilimlem1  22606  chtppilim  22608  chto1ub  22609  vmadivsum  22615  rplogsumlem1  22617  rplogsumlem2  22618  dchrisum0lem1a  22619  rpvmasumlem  22620  dchrisumlem1  22622  dchrisumlem2  22623  dchrvmasumlem2  22631  dchrisum0flblem1  22641  dchrisum0flblem2  22642  dchrisum0lem1b  22648  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem3  22652  dchrisum0  22653  mudivsum  22663  mulogsumlem  22664  mulog2sumlem1  22667  mulog2sumlem2  22668  2vmadivsumlem  22673  chpdifbndlem1  22686  selberg3lem1  22690  selberg4lem1  22693  pntrlog2bndlem1  22710  pntrlog2bndlem2  22711  pntrlog2bndlem3  22712  pntrlog2bndlem4  22713  pntpbnd1a  22718  pntpbnd1  22719  pntpbnd2  22720  pntibndlem2  22724  pntibndlem3  22725  pntlemd  22727  pntlemc  22728  pntlemb  22730  pntlemg  22731  pntlemh  22732  pntlemr  22735  pntlemf  22738  pntlemo  22740  abvcxp  22748  ostth2lem1  22751  padicabv  22763  ostth2lem2  22767  ostth2lem3  22768  ostth2lem4  22769  ostth2  22770  ostth3  22771  ttgcontlem1  22953  axpaschlem  23008  axcontlem8  23039  umgraex  23079  nvabs  23883  nmooge0  23989  nmoolb  23993  siii  24075  minvecolem2  24098  minvecolem4  24103  minvecolem5  24104  hlipgt0  24137  normge0  24350  normpyc  24370  pjhthlem1  24616  pjige0i  24915  nmoplb  25133  nmfnlb  25150  branmfn  25331  pjssdif2i  25400  stlei  25466  mul2lt0rgt0  25863  xlt2addrd  25875  eliccelico  25889  elicoelioo  25890  bcm1n  25901  omndmul2  25998  archirngz  26029  archiabllem2c  26035  xrge0tsmsd  26105  ofldchr  26134  xrge0iifiso  26218  nexple  26301  gsumesum  26363  esumcst  26367  esumpcvgval  26380  esumcvg  26388  measssd  26482  measunl  26483  sibfof  26573  oddpwdc  26584  eulerpartlemgc  26592  iwrdsplit  26617  ballotlemsgt1  26740  ballotlemsel1i  26742  sgnmul  26772  signsply0  26799  signstfvc  26822  signsvtp  26831  signsvfpn  26833  zetacvg  26848  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamcvg2  26888  subfaclim  26923  erdszelem7  26932  erdszelem8  26933  cvmliftlem2  27022  snmlff  27065  sinccvglem  27163  climlec3  27247  clim2div  27250  ntrivcvgtail  27261  iprodclim2  27345  iprodclim3  27346  faclim  27398  dvdspw  27402  nodense  27676  nobndup  27687  lxflflp1  28262  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  itg2addnclem  28284  itg2addnclem3  28286  itg2gt0cn  28288  itggt0cn  28305  ftc1anclem5  28312  ftc1anclem7  28314  ftc1anclem8  28315  fnejoin1  28430  isbnd3  28524  ssbnd  28528  heiborlem8  28558  bfplem2  28563  rrncmslem  28572  rrnequiv  28575  rrntotbnd  28576  eldioph2lem1  28940  lzenom  28950  irrapxlem1  29005  irrapxlem4  29008  irrapxlem5  29009  pell14qrgt0  29042  pell1qrge1  29053  pell1qrgap  29057  pellfundge  29065  pellfundex  29069  pellfund14  29081  rmspecsqrnq  29089  rmxypos  29132  ltrmynn0  29133  ltrmxnn0  29134  jm2.24nn  29144  jm2.17b  29146  jm2.17c  29147  jm2.24  29148  congadd  29151  congsym  29153  congneg  29154  congid  29156  mzpcong  29157  acongrep  29165  acongeq  29168  jm2.18  29179  jm2.19  29184  jm2.23  29187  jm2.25  29190  jm2.26lem3  29192  jm2.15nn0  29194  jm2.16nn0  29195  jm2.27a  29196  jm2.27c  29198  jm3.1lem1  29208  idomrootle  29402  idomsubgmo  29405  cncmpmax  29596  fmul01  29603  fmul01lt1lem1  29607  climdivf  29628  stoweidlem1  29639  stoweidlem16  29654  stoweidlem18  29656  stoweidlem24  29662  stoweidlem26  29664  stoweidlem36  29674  stoweidlem38  29676  stoweidlem41  29679  stoweidlem42  29680  stoweidlem44  29682  stoweidlem45  29683  stoweidlem48  29686  stoweidlem62  29700  wallispilem5  29707  stirlinglem1  29712  stirlinglem5  29716  stirlinglem7  29718  stirlinglem8  29719  stirlinglem9  29720  stirlinglem11  29722  rlimdmafv  29926  2elfz2melfz  30045  clwlkisclwwlk2  30295  clwwlkndivn  30354  clwlkf1clwwlklem1  30362  wwlkextproplem3  30405  lcv1  32256  lsatcv0eq  32262  lsatcvat3  32267  cvlsupr2  32558  hlatlej2  32590  cvrval4N  32628  cvratlem  32635  atcvr0eq  32640  2atlt  32653  atbtwnex  32662  athgt  32670  1cvrat  32690  ps-1  32691  hlatexch3N  32694  hlatexch4  32695  3atlem2  32698  atcvrlln2  32733  lplnexllnN  32778  4atlem3a  32811  4atlem10b  32819  4atlem11b  32822  4atlem12b  32825  2lplnja  32833  dalemply  32868  dalemsly  32869  dalem1  32873  dalem6  32882  dalem7  32883  dalem-cly  32885  dalem11  32888  dalem12  32889  dalem16  32893  dalem17  32894  dalem38  32924  dalem44  32930  dalem61  32947  lnatexN  32993  lncvrat  32996  lncmp  32997  paddasslem2  33035  dalawlem3  33087  dalawlem6  33090  dalawlem11  33095  lhpmcvr  33237  lhp2atne  33248  lhp2at0ne  33250  lautj  33307  trlval4  33402  cdlemc2  33406  cdlemc5  33409  cdleme3b  33443  cdleme11c  33475  cdleme19a  33517  cdleme20j  33532  cdleme22f  33560  cdleme23c  33565  cdleme26f2ALTN  33578  cdleme26f2  33579  cdleme35fnpq  33663  cdleme48bw  33716  cdlemg10a  33854  cdlemg11b  33856  cdlemg17g  33881  cdlemg18c  33894  cdlemi1  34032  cdlemk52  34168  dia2dimlem1  34279  dihord1  34433  dihjatcclem4  34636
  Copyright terms: Public domain W3C validator