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

Theorem breqtrrd 4478
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrrd.1
breqtrrd.2
Assertion
Ref Expression
breqtrrd

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2
2 breqtrrd.2 . . 3
32eqcomd 2465 . 2
41, 3breqtrd 4476 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  marypha1lem  7913  marypha2  7919  unxpwdom  8036  uncdadom  8572  cdacomen  8582  cdaassen  8583  xpcdaen  8584  onacda  8598  infcdaabs  8607  cfss  8666  tskuni  9182  ltexnq  9374  xrmax1  11405  xrmax2  11406  max1ALT  11416  qbtwnxr  11428  xleadd1a  11474  xlt2add  11481  xlesubadd  11484  xmulgt0  11504  xlemul1a  11509  xov1plusxeqvd  11695  uzsubsubfz  11736  fzctr  11816  flflp1  11944  ceilge  11973  modge0  12005  modlt  12006  modid  12020  modaddmodup  12050  sermono  12139  seqf1olem1  12146  seqf1olem2  12147  leexp1a  12224  sqgt0  12236  sqge0  12244  nnlesq  12271  expnbnd  12295  expmulnbnd  12298  discr1  12302  facwordi  12367  faclbnd5  12376  hashdom  12447  brfi1uzind  12532  ccatws1n0  12636  swrds2  12883  cjmulge0  12979  resqrtcl  13087  absge0  13120  sqreulem  13192  amgm2  13202  rlimdm  13374  rlimge0  13404  reccn2  13419  climle  13462  climserle  13485  isercoll2  13491  iseraltlem1  13504  iseralt  13507  isumclim2  13573  isumclim3  13574  isumge0  13581  fsumless  13610  cvgcmp  13630  cvgcmpce  13632  abscvgcvg  13633  isumsup2  13658  isumltss  13660  climcndslem1  13661  climcnds  13663  supcvg  13667  harmonic  13670  expcnv  13675  explecnv  13676  cvgrat  13692  mertenslem1  13693  mertenslem2  13694  clim2div  13698  ntrivcvgtail  13709  iprodclim2  13792  iprodclim3  13793  efcvg  13820  ege2le3  13825  efaddlem  13828  eftlub  13844  effsumlt  13846  tanhlt1  13895  ef01bndlem  13919  sin02gt0  13927  rpnnen2lem4  13951  ruclem2  13965  ruclem3  13966  ruclem9  13971  iddvdsexp  14007  dvdsadd  14024  dvdsfac  14041  dvdsmod  14043  3dvds  14050  divalglem1  14052  bitsfzo  14085  bitsmod  14086  bitscmp  14088  bitsinv1lem  14091  sadcaddlem  14107  sadadd3  14111  sadaddlem  14116  dvdssqim  14191  dvdsmulgcd  14192  nn0seqcvgd  14199  sqnprm  14239  mulgcddvds  14245  qredeq  14247  isprm6  14250  nonsq  14292  hashdvds  14305  prmdiv  14315  odzdvds  14322  omoe  14336  pythagtriplem4  14343  pcpre1  14366  pcdvdsb  14392  pcz  14404  pcprmpw2  14405  pcaddlem  14407  pcadd  14408  pcadd2  14409  pcmpt  14411  pcmptdvds  14413  fldivp1  14416  pcfaclem  14417  pockthlem  14423  prmreclem1  14434  prmreclem3  14436  prmreclem5  14438  prmreclem6  14439  4sqlem6  14461  4sqlem8  14463  4sqlem11  14473  4sqlem12  14474  4sqlem14  14476  4sqlem16  14478  vdwlem3  14501  vdwlem9  14507  vdwlem10  14508  vdwlem12  14510  ramub1lem2  14545  invfuc  15343  ple1  15674  eqgen  16254  lagsubg  16263  pgpfi  16625  sylow2alem2  16638  sylow2a  16639  sylow3lem4  16650  efgsrel  16752  odadd1  16854  odadd2  16855  gexex  16859  lt6abl  16897  dprd2d2  17093  dmdprdpr  17098  ablfacrp2  17118  ablfac1c  17122  pgpfaclem1  17132  ablfac2  17140  dvdsrmul1  17302  unitmulclb  17314  subrguss  17444  abvres  17488  ply1coefsupp  18336  evl1gsumadd  18394  znfld  18599  znunit  18602  frlmisfrlm  18883  matgsum  18939  pm2mpcl  19298  psmetxrge0  20817  isxmet2d  20830  mettri  20855  xmettri3  20856  mettri3  20857  xmetrtri2  20859  prdsxmetlem  20871  imasdsf1olem  20876  xblss2ps  20904  blss2ps  20906  blss2  20907  blssps  20927  blss  20928  prdsbl  20994  dscmet  21093  nmge0  21136  nmmtri  21141  nlmvscnlem2  21194  nrginvrcnlem  21199  nmoix  21236  nmoleub  21238  blcvx  21303  xrsxmet  21314  opnreen  21336  xrge0tsms  21339  icopnfcnv  21442  xrhmeo  21446  lebnumii  21466  pcophtb  21529  pi1grplem  21549  nmoleub2lem  21597  ipcau2  21677  tchcphlem1  21678  ipcau  21681  ipcnlem2  21684  rrxcph  21824  minveclem2  21841  minveclem3b  21843  pjthlem1  21852  pjthlem2  21853  ivthlem3  21865  ivth2  21867  ovolfsf  21883  ovolsslem  21895  ovollb2lem  21899  ovollb2  21900  ovolctb  21901  ovolfiniun  21912  ovolicc1  21927  ovolicc2lem4  21931  ovolicc2  21933  nulmbl2  21947  unmbl  21948  ioombl1lem4  21971  uniioombllem4  21995  uniioombllem6  21997  volivth  22016  vitalilem4  22020  itg1ge0  22093  itg1ge0a  22118  itg1lea  22119  itg1climres  22121  mbfi1fseqlem5  22126  itg2ub  22140  itg2seq  22149  itg2uba  22150  itg2splitlem  22155  itg2split  22156  itg2monolem3  22159  itg2mono  22160  itg2i1fseq2  22163  itg2addlem  22165  iblss  22211  itggt0  22248  dvferm2lem  22387  dvlip  22394  dvivthlem1  22409  dvfsumlem2  22428  dvfsumlem3  22429  ftc1lem4  22440  ply1divmo  22536  ply1remlem  22563  fta1glem2  22567  ig1pdvds  22577  plyeq0lem  22607  plydiveu  22694  fta1lem  22703  vieta1lem2  22707  aaliou3lem2  22739  aaliou3lem8  22741  ulmcn  22794  mtest  22799  itgulm  22803  radcnvlem1  22808  radcnvlt1  22813  dvradcnv  22816  pserdvlem2  22823  abelthlem2  22827  abelthlem6  22831  abelthlem7  22833  abelthlem9  22835  tangtx  22898  sinq12gt0  22900  sineq0  22914  cosordlem  22918  tanord  22925  tanregt0  22926  logrnaddcl  22962  logcj  22991  argregt0  22995  argrege0  22996  argimgt0  22997  argimlt0  22998  logimul  22999  logneg2  23000  logdivlti  23005  divlogrlim  23016  logcnlem3  23025  logcnlem4  23026  dvlog2lem  23033  logtayl  23041  rpcxpcl  23057  cxpsqrtlem  23083  cxpaddle  23126  isosctrlem1  23152  asinlem3a  23201  asinlem3  23202  asinneg  23217  asinsinlem  23222  asinsin  23223  atanlogaddlem  23244  atanlogadd  23245  atanlogsublem  23246  atanlogsub  23247  atantan  23254  atanbndlem  23256  atantayl  23268  leibpi  23273  birthdaylem3  23283  areaf  23291  cxploglim  23307  jensenlem2  23317  jensen  23318  logdiflbnd  23324  harmonicbnd4  23340  fsumharmonic  23341  wilthlem2  23343  ftalem1  23346  ftalem2  23347  ftalem5  23350  basellem6  23359  basellem8  23361  basellem9  23362  chtge0  23386  chtublem  23486  logexprlim  23500  perfectlem1  23504  bcmax  23553  bposlem1  23559  bposlem2  23560  bposlem6  23564  bposlem7  23565  lgsdilem2  23606  lgsqrlem4  23619  lgsquadlem1  23629  2sqlem3  23641  2sqlem8  23647  2sqblem  23652  chebbnd1lem2  23655  chtppilimlem1  23658  chtppilim  23660  chto1ub  23661  vmadivsum  23667  rplogsumlem1  23669  rplogsumlem2  23670  dchrisum0lem1a  23671  rpvmasumlem  23672  dchrisumlem1  23674  dchrisumlem2  23675  dchrvmasumlem2  23683  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem3  23704  dchrisum0  23705  mudivsum  23715  mulogsumlem  23716  mulog2sumlem1  23719  mulog2sumlem2  23720  2vmadivsumlem  23725  chpdifbndlem1  23738  selberg3lem1  23742  selberg4lem1  23745  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2  23776  pntibndlem3  23777  pntlemd  23779  pntlemc  23780  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemr  23787  pntlemf  23790  pntlemo  23792  abvcxp  23800  ostth2lem1  23803  padicabv  23815  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth2  23822  ostth3  23823  legso  23985  krippenlem  24067  midex  24111  ttgcontlem1  24188  axpaschlem  24243  axcontlem8  24274  umgraex  24323  wwlkextproplem3  24743  clwlkisclwwlk2  24790  clwwlkndivn  24837  clwlkf1clwwlklem1  24846  ex-ind-dvds  25170  nvabs  25576  nmooge0  25682  nmoolb  25686  siii  25768  minvecolem2  25791  minvecolem4  25796  minvecolem5  25797  hlipgt0  25830  normge0  26043  normpyc  26063  pjhthlem1  26309  pjige0i  26608  nmoplb  26826  nmfnlb  26843  branmfn  27024  pjssdif2i  27093  stlei  27159  mul2lt0rgt0  27566  xlt2addrd  27578  eliccelico  27588  elicoelioo  27589  bcm1n  27600  2sqmod  27636  omndmul2  27702  archirngz  27733  archiabllem2c  27739  xrge0tsmsd  27775  ofldchr  27804  locfinreflem  27843  xrge0iifiso  27917  nexple  28005  gsumesum  28067  esumcst  28071  esumpcvgval  28084  esumcvg  28092  measssd  28186  measunl  28187  sibfof  28282  oddpwdc  28293  eulerpartlemgc  28301  iwrdsplit  28326  ballotlemsgt1  28449  ballotlemsel1i  28451  sgnmul  28481  signsply0  28508  signstfvc  28531  signsvtp  28540  signsvfpn  28542  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamcvg2  28597  subfaclim  28632  erdszelem7  28641  erdszelem8  28642  cvmliftlem2  28731  snmlff  28774  sinccvglem  29038  climlec3  29120  faclim  29171  dvdspw  29175  nodense  29449  nobndup  29460  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnclem3  30068  itg2gt0cn  30070  itggt0cn  30087  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  fnejoin1  30186  isbnd3  30280  ssbnd  30284  heiborlem8  30314  bfplem2  30319  rrncmslem  30328  rrnequiv  30331  rrntotbnd  30332  eldioph2lem1  30693  lzenom  30703  irrapxlem1  30758  irrapxlem4  30761  irrapxlem5  30762  pell14qrgt0  30795  pell1qrge1  30806  pell1qrgap  30810  pellfundge  30818  pellfundex  30822  pellfund14  30834  rmspecsqrtnq  30842  rmxypos  30885  ltrmynn0  30886  ltrmxnn0  30887  jm2.24nn  30897  jm2.17b  30899  jm2.17c  30900  jm2.24  30901  congadd  30904  congsym  30906  congneg  30907  congid  30909  mzpcong  30910  acongrep  30918  acongeq  30921  jm2.18  30930  jm2.19  30935  jm2.23  30938  jm2.25  30941  jm2.26lem3  30943  jm2.15nn0  30945  jm2.16nn0  30946  jm2.27a  30947  jm2.27c  30949  jm3.1lem1  30959  idomrootle  31152  idomsubgmo  31155  dvgrat  31193  radcnvrat  31195  dvdslcm  31204  lcmgcdlem  31212  binomcxplemnn0  31254  binomcxplemnotnn0  31261  cncmpmax  31407  zltlesub  31468  lt2addmuld  31473  fmul01  31574  fmul01lt1lem1  31578  climdivf  31618  sumnnodd  31636  dvdivbd  31720  volge0  31760  stoweidlem1  31783  stoweidlem16  31798  stoweidlem18  31800  stoweidlem24  31806  stoweidlem26  31808  stoweidlem36  31818  stoweidlem38  31820  stoweidlem41  31823  stoweidlem42  31824  stoweidlem44  31826  stoweidlem45  31827  stoweidlem48  31830  stoweidlem62  31844  wallispilem5  31851  stirlinglem1  31856  stirlinglem5  31860  stirlinglem7  31862  stirlinglem8  31863  stirlinglem9  31864  stirlinglem11  31866  fourierdlem4  31893  fourierdlem10  31899  fourierdlem37  31926  fourierdlem47  31936  fourierdlem72  31961  fourierdlem74  31963  fourierdlem79  31968  fourierdlem82  31971  fourierdlem89  31978  fourierdlem91  31980  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  etransclem24  32041  etransclem25  32042  etransclem28  32045  etransclem37  32054  etransclem38  32055  etransclem44  32061  rlimdmafv  32262  2elfz2melfz  32334  usgedgleord  32419  cznnring  32764  rhmsubcrngc  32837  altgsumbcALT  32942  lcv1  34766  lsatcv0eq  34772  lsatcvat3  34777  cvlsupr2  35068  hlatlej2  35100  cvrval4N  35138  cvratlem  35145  atcvr0eq  35150  2atlt  35163  atbtwnex  35172  athgt  35180  1cvrat  35200  ps-1  35201  hlatexch3N  35204  hlatexch4  35205  3atlem2  35208  atcvrlln2  35243  lplnexllnN  35288  4atlem3a  35321  4atlem10b  35329  4atlem11b  35332  4atlem12b  35335  2lplnja  35343  dalemply  35378  dalemsly  35379  dalem1  35383  dalem6  35392  dalem7  35393  dalem-cly  35395  dalem11  35398  dalem12  35399  dalem16  35403  dalem17  35404  dalem38  35434  dalem44  35440  dalem61  35457  lnatexN  35503  lncvrat  35506  lncmp  35507  paddasslem2  35545  dalawlem3  35597  dalawlem6  35600  dalawlem11  35605  lhpmcvr  35747  lhp2atne  35758  lhp2at0ne  35760  lautj  35817  trlval4  35913  cdlemc2  35917  cdlemc5  35920  cdleme3b  35954  cdleme11c  35986  cdleme19a  36029  cdleme20j  36044  cdleme22f  36072  cdleme23c  36077  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme35fnpq  36175  cdleme48bw  36228  cdlemg10a  36366  cdlemg11b  36368  cdlemg17g  36393  cdlemg18c  36406  cdlemi1  36544  cdlemk52  36680  dia2dimlem1  36791  dihord1  36945  dihjatcclem4  37148  inductionexd  37967  imo72b2  37993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator