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

Theorem breqtrrd 4313
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 2443 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 4311 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  marypha1lem  7675  marypha2  7681  unxpwdom  7796  uncdadom  8332  cdacomen  8342  cdaassen  8343  xpcdaen  8344  onacda  8358  infcdaabs  8367  cfss  8426  tskuni  8942  ltexnq  9136  xrmax1  11139  xrmax2  11140  max1ALT  11150  qbtwnxr  11162  xleadd1a  11208  xlt2add  11215  xlesubadd  11218  xmulgt0  11238  xlemul1a  11243  xov1plusxeqvd  11423  uzsubsubfz  11463  fzctr  11521  ceilge  11677  modge0  11709  modlt  11710  modid  11724  modaddmodup  11754  sermono  11830  seqf1olem1  11837  seqf1olem2  11838  leexp1a  11914  sqgt0  11926  sqge0  11934  nnlesq  11961  expnbnd  11985  expmulnbnd  11988  discr1  11992  facwordi  12057  faclbnd5  12066  hashdom  12134  brfi1uzind  12211  ccatws1n0  12302  swrds2  12537  cjmulge0  12627  resqrcl  12735  absge0  12768  sqreulem  12839  amgm2  12849  rlimdm  13021  rlimge0  13051  reccn2  13066  climle  13109  climserle  13132  isercoll2  13138  iseraltlem1  13151  iseralt  13154  isumclim2  13217  isumclim3  13218  isumge0  13225  fsumless  13251  cvgcmp  13271  cvgcmpce  13273  abscvgcvg  13274  isumsup2  13301  isumltss  13303  climcndslem1  13304  climcnds  13306  supcvg  13310  harmonic  13313  expcnv  13318  explecnv  13319  cvgrat  13335  mertenslem1  13336  mertenslem2  13337  efcvg  13362  ege2le3  13367  efaddlem  13370  eftlub  13385  effsumlt  13387  tanhlt1  13436  ef01bndlem  13460  sin02gt0  13468  rpnnen2lem4  13492  ruclem2  13506  ruclem3  13507  ruclem9  13512  iddvdsexp  13548  dvdsadd  13563  dvdsfac  13580  dvdsmod  13582  3dvds  13588  divalglem1  13590  bitsfzo  13623  bitsmod  13624  bitscmp  13626  bitsinv1lem  13629  sadcaddlem  13645  sadadd3  13649  sadaddlem  13654  dvdssqim  13729  dvdsmulgcd  13730  nn0seqcvgd  13737  sqnprm  13776  mulgcddvds  13782  qredeq  13784  isprm6  13787  nonsq  13829  hashdvds  13842  prmdiv  13852  odzdvds  13859  omoe  13871  pythagtriplem4  13878  pcpre1  13901  pcdvdsb  13927  pcz  13939  pcprmpw2  13940  pcaddlem  13942  pcadd  13943  pcadd2  13944  pcmpt  13946  pcmptdvds  13948  fldivp1  13951  pcfaclem  13952  pockthlem  13958  prmreclem1  13969  prmreclem3  13971  prmreclem5  13973  prmreclem6  13974  4sqlem6  13996  4sqlem8  13998  4sqlem11  14008  4sqlem12  14009  4sqlem14  14011  4sqlem16  14013  vdwlem3  14036  vdwlem9  14042  vdwlem10  14043  vdwlem12  14045  ramub1lem2  14080  invfuc  14876  ple1  15206  eqgen  15725  lagsubg  15734  pgpfi  16095  sylow2alem2  16108  sylow2a  16109  sylow3lem4  16120  efgsrel  16222  odadd1  16321  odadd2  16322  gexex  16326  lt6abl  16362  dprd2d2  16533  dmdprdpr  16538  ablfacrp2  16558  ablfac1c  16562  pgpfaclem1  16572  ablfac2  16580  dvdsrmul1  16735  unitmulclb  16747  subrguss  16860  abvres  16904  ply1coefsupp  17725  evl1gsumadd  17772  znfld  17973  znunit  17976  frlmisfrlm  18257  psmetxrge0  19869  isxmet2d  19882  mettri  19907  xmettri3  19908  mettri3  19909  xmetrtri2  19911  prdsxmetlem  19923  imasdsf1olem  19928  xblss2ps  19956  blss2ps  19958  blss2  19959  blssps  19979  blss  19980  prdsbl  20046  dscmet  20145  nmge0  20188  nmmtri  20193  nlmvscnlem2  20246  nrginvrcnlem  20251  nmoix  20288  nmoleub  20290  blcvx  20355  xrsxmet  20366  opnreen  20388  xrge0tsms  20391  icopnfcnv  20494  xrhmeo  20498  lebnumii  20518  pcophtb  20581  pi1grplem  20601  nmoleub2lem  20649  ipcau2  20729  tchcphlem1  20730  ipcau  20733  ipcnlem2  20736  rrxcph  20876  minveclem2  20893  minveclem3b  20895  pjthlem1  20904  pjthlem2  20905  ivthlem3  20917  ivth2  20919  ovolfsf  20935  ovolsslem  20947  ovollb2lem  20951  ovollb2  20952  ovolctb  20953  ovolfiniun  20964  ovolicc1  20979  ovolicc2lem4  20983  ovolicc2  20985  nulmbl2  20998  unmbl  20999  ioombl1lem4  21022  uniioombllem4  21046  uniioombllem6  21048  volivth  21067  vitalilem4  21071  itg1ge0  21144  itg1ge0a  21169  itg1lea  21170  itg1climres  21172  mbfi1fseqlem5  21177  itg2ub  21191  itg2seq  21200  itg2uba  21201  itg2splitlem  21206  itg2split  21207  itg2monolem3  21210  itg2mono  21211  itg2i1fseq2  21214  itg2addlem  21216  iblss  21262  itggt0  21299  dvferm2lem  21438  dvlip  21445  dvivthlem1  21460  dvfsumlem2  21479  dvfsumlem3  21480  ftc1lem4  21491  ply1divmo  21587  ply1remlem  21614  fta1glem2  21618  ig1pdvds  21628  plyeq0lem  21658  plydiveu  21744  fta1lem  21753  vieta1lem2  21757  aaliou3lem2  21789  aaliou3lem8  21791  ulmcn  21844  mtest  21849  itgulm  21853  radcnvlem1  21858  radcnvlt1  21863  dvradcnv  21866  pserdvlem2  21873  abelthlem2  21877  abelthlem6  21881  abelthlem7  21883  abelthlem9  21885  tangtx  21947  sinq12gt0  21949  sineq0  21963  cosordlem  21967  tanord  21974  tanregt0  21975  logrnaddcl  22006  logcj  22035  argregt0  22039  argrege0  22040  argimgt0  22041  argimlt0  22042  logimul  22043  logneg2  22044  logdivlti  22049  divlogrlim  22060  logcnlem3  22069  logcnlem4  22070  dvlog2lem  22077  logtayl  22085  rpcxpcl  22101  cxpsqrlem  22127  cxpaddle  22170  isosctrlem1  22196  asinlem3a  22245  asinlem3  22246  asinneg  22261  asinsinlem  22266  asinsin  22267  atanlogaddlem  22288  atanlogadd  22289  atanlogsublem  22290  atanlogsub  22291  atantan  22298  atanbndlem  22300  atantayl  22312  leibpi  22317  birthdaylem3  22327  areaf  22335  cxploglim  22351  jensenlem2  22361  jensen  22362  logdiflbnd  22368  harmonicbnd4  22384  fsumharmonic  22385  wilthlem2  22387  ftalem1  22390  ftalem2  22391  ftalem5  22394  basellem6  22403  basellem8  22405  basellem9  22406  chtge0  22430  chtublem  22530  logexprlim  22544  perfectlem1  22548  bcmax  22597  bposlem1  22603  bposlem2  22604  bposlem6  22608  bposlem7  22609  lgsdilem2  22650  lgsqrlem4  22663  lgsquadlem1  22673  2sqlem3  22685  2sqlem8  22691  2sqblem  22696  chebbnd1lem2  22699  chtppilimlem1  22702  chtppilim  22704  chto1ub  22705  vmadivsum  22711  rplogsumlem1  22713  rplogsumlem2  22714  dchrisum0lem1a  22715  rpvmasumlem  22716  dchrisumlem1  22718  dchrisumlem2  22719  dchrvmasumlem2  22727  dchrisum0flblem1  22737  dchrisum0flblem2  22738  dchrisum0lem1b  22744  dchrisum0lem1  22745  dchrisum0lem2a  22746  dchrisum0lem3  22748  dchrisum0  22749  mudivsum  22759  mulogsumlem  22760  mulog2sumlem1  22763  mulog2sumlem2  22764  2vmadivsumlem  22769  chpdifbndlem1  22782  selberg3lem1  22786  selberg4lem1  22789  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntpbnd1a  22814  pntpbnd1  22815  pntpbnd2  22816  pntibndlem2  22820  pntibndlem3  22821  pntlemd  22823  pntlemc  22824  pntlemb  22826  pntlemg  22827  pntlemh  22828  pntlemr  22831  pntlemf  22834  pntlemo  22836  abvcxp  22844  ostth2lem1  22847  padicabv  22859  ostth2lem2  22863  ostth2lem3  22864  ostth2lem4  22865  ostth2  22866  ostth3  22867  krippenlem  23061  ttgcontlem1  23099  axpaschlem  23154  axcontlem8  23185  umgraex  23225  nvabs  24029  nmooge0  24135  nmoolb  24139  siii  24221  minvecolem2  24244  minvecolem4  24249  minvecolem5  24250  hlipgt0  24283  normge0  24496  normpyc  24516  pjhthlem1  24762  pjige0i  25061  nmoplb  25279  nmfnlb  25296  branmfn  25477  pjssdif2i  25546  stlei  25612  mul2lt0rgt0  26007  xlt2addrd  26019  eliccelico  26035  elicoelioo  26036  bcm1n  26047  omndmul2  26143  archirngz  26174  archiabllem2c  26180  xrge0tsmsd  26221  ofldchr  26250  xrge0iifiso  26334  nexple  26417  gsumesum  26479  esumcst  26483  esumpcvgval  26496  esumcvg  26504  measssd  26598  measunl  26599  sibfof  26695  oddpwdc  26706  eulerpartlemgc  26714  iwrdsplit  26739  ballotlemsgt1  26862  ballotlemsel1i  26864  sgnmul  26894  signsply0  26921  signstfvc  26944  signsvtp  26953  signsvfpn  26955  zetacvg  26970  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamcvg2  27010  subfaclim  27045  erdszelem7  27054  erdszelem8  27055  cvmliftlem2  27144  snmlff  27187  sinccvglem  27286  climlec3  27370  clim2div  27373  ntrivcvgtail  27384  iprodclim2  27468  iprodclim3  27469  faclim  27521  dvdspw  27525  nodense  27799  nobndup  27810  lxflflp1  28392  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  itg2addnclem  28414  itg2addnclem3  28416  itg2gt0cn  28418  itggt0cn  28435  ftc1anclem5  28442  ftc1anclem7  28444  ftc1anclem8  28445  fnejoin1  28560  isbnd3  28654  ssbnd  28658  heiborlem8  28688  bfplem2  28693  rrncmslem  28702  rrnequiv  28705  rrntotbnd  28706  eldioph2lem1  29069  lzenom  29079  irrapxlem1  29134  irrapxlem4  29137  irrapxlem5  29138  pell14qrgt0  29171  pell1qrge1  29182  pell1qrgap  29186  pellfundge  29194  pellfundex  29198  pellfund14  29210  rmspecsqrnq  29218  rmxypos  29261  ltrmynn0  29262  ltrmxnn0  29263  jm2.24nn  29273  jm2.17b  29275  jm2.17c  29276  jm2.24  29277  congadd  29280  congsym  29282  congneg  29283  congid  29285  mzpcong  29286  acongrep  29294  acongeq  29297  jm2.18  29308  jm2.19  29313  jm2.23  29316  jm2.25  29319  jm2.26lem3  29321  jm2.15nn0  29323  jm2.16nn0  29324  jm2.27a  29325  jm2.27c  29327  jm3.1lem1  29337  idomrootle  29531  idomsubgmo  29534  cncmpmax  29725  fmul01  29732  fmul01lt1lem1  29736  climdivf  29756  stoweidlem1  29767  stoweidlem16  29782  stoweidlem18  29784  stoweidlem24  29790  stoweidlem26  29792  stoweidlem36  29802  stoweidlem38  29804  stoweidlem41  29807  stoweidlem42  29808  stoweidlem44  29810  stoweidlem45  29811  stoweidlem48  29814  stoweidlem62  29828  wallispilem5  29835  stirlinglem1  29840  stirlinglem5  29844  stirlinglem7  29846  stirlinglem8  29847  stirlinglem9  29848  stirlinglem11  29850  rlimdmafv  30054  2elfz2melfz  30173  clwlkisclwwlk2  30423  clwwlkndivn  30482  clwlkf1clwwlklem1  30490  wwlkextproplem3  30533  altgsumbcALT  30719  matgsum  30822  lcv1  32579  lsatcv0eq  32585  lsatcvat3  32590  cvlsupr2  32881  hlatlej2  32913  cvrval4N  32951  cvratlem  32958  atcvr0eq  32963  2atlt  32976  atbtwnex  32985  athgt  32993  1cvrat  33013  ps-1  33014  hlatexch3N  33017  hlatexch4  33018  3atlem2  33021  atcvrlln2  33056  lplnexllnN  33101  4atlem3a  33134  4atlem10b  33142  4atlem11b  33145  4atlem12b  33148  2lplnja  33156  dalemply  33191  dalemsly  33192  dalem1  33196  dalem6  33205  dalem7  33206  dalem-cly  33208  dalem11  33211  dalem12  33212  dalem16  33216  dalem17  33217  dalem38  33247  dalem44  33253  dalem61  33270  lnatexN  33316  lncvrat  33319  lncmp  33320  paddasslem2  33358  dalawlem3  33410  dalawlem6  33413  dalawlem11  33418  lhpmcvr  33560  lhp2atne  33571  lhp2at0ne  33573  lautj  33630  trlval4  33725  cdlemc2  33729  cdlemc5  33732  cdleme3b  33766  cdleme11c  33798  cdleme19a  33840  cdleme20j  33855  cdleme22f  33883  cdleme23c  33888  cdleme26f2ALTN  33901  cdleme26f2  33902  cdleme35fnpq  33986  cdleme48bw  34039  cdlemg10a  34177  cdlemg11b  34179  cdlemg17g  34204  cdlemg18c  34217  cdlemi1  34355  cdlemk52  34491  dia2dimlem1  34602  dihord1  34756  dihjatcclem4  34959
  Copyright terms: Public domain W3C validator