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

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

Proof of Theorem breqtrd
StepHypRef Expression
1 breqtrd.1 . 2
2 breqtrd.2 . . 3
32breq2d 4464 . 2
41, 3mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  breqtrrd  4478  syl5breq  4487  domunsn  7687  mapdom2  7708  phplem4  7719  mapfien2  7888  wemaplem2  7993  infdifsn  8094  cantnff  8114  infxpenlem  8412  pwcda1  8595  pwcdadom  8617  infmap2  8619  ssfin4  8711  canthp1lem1  9051  nqereq  9334  ltexnq  9374  ltbtwnnq  9377  add20  10089  mullt0  10097  ltm1  10407  recgt0  10411  prodgt0  10412  prodge0  10414  ltmul1a  10416  mulge0b  10437  recp1lt1  10468  recreclt  10469  ledivp1  10472  ledivp1i  10496  ltdivp1i  10497  ltaddrp2d  11315  xleadd1a  11474  xov1plusxeqvd  11695  fz01en  11742  fzonmapblen  11868  fladdz  11958  flhalf  11962  fldiv  11987  modsubdir  12055  fzen2  12079  serle  12162  ltexp2a  12217  leexp2a  12221  exple1  12225  expubnd  12226  bernneq  12292  expmulnbnd  12298  discr1  12302  discr  12303  faclbnd6  12377  hashfz  12485  hashfun  12495  seqcoll  12512  sqeqd  12999  sqrlem7  13082  sqrtge0  13091  sqrtneglem  13100  abslt  13147  absle  13148  abstri  13163  rlimge0  13404  reccn2  13419  climaddc2  13458  isercolllem1  13487  caucvgrlem  13495  summolem2a  13537  isumge0  13581  fsumle  13613  fsumlt  13614  o1fsum  13627  supcvg  13667  expcnv  13675  geolim  13679  geolim2  13680  georeclim  13681  geo2lim  13684  mertenslem1  13693  mertens  13695  prodmolem2a  13741  efcllem  13813  ef0lem  13814  efgt0  13838  eftlub  13844  eflt  13852  sinbnd  13915  cosbnd  13916  ef01bndlem  13919  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  eirrlem  13937  rpnnen2lem11  13958  rpnnen2  13959  ruclem11  13973  dvdssub2  14023  dvdsadd2b  14028  dvdsexp  14042  3dvds  14050  bitsfzolem  14084  bitsinv1lem  14091  bezoutlem4  14179  dvdsgcd  14181  dvdsmulgcd  14192  nn0seqcvgd  14199  prmind2  14228  rpmulgcd2  14246  qredeq  14247  rpdvds  14265  divdenle  14282  hashdvds  14305  phimullem  14309  eulerthlem2  14312  prmdiveq  14316  prmdivdiv  14317  opoe  14335  pythagtriplem4  14343  pythagtriplem10  14344  pythagtriplem19  14357  iserodd  14359  pcpre1  14366  pcadd2  14409  qexpz  14420  expnprm  14421  pockthlem  14423  prmreclem2  14435  prmreclem3  14436  4sqlem7  14462  4sqlem10  14465  4sqlem11  14473  4sqlem12  14474  4sqlem14  14476  4sqlem15  14477  4sqlem16  14478  0ram  14538  ffthiso  15298  latmlej12  15721  qusgrp  16256  pgpfi1  16615  sylow1lem4  16621  sylow1lem5  16622  odcau  16624  pgpfi  16625  pgpssslw  16634  sylow3lem4  16650  sylow3lem6  16652  efgsfo  16757  frgp0  16778  odadd1  16854  odadd2  16855  odadd  16856  gexexlem  16858  lt6abl  16897  gsumzsubmcl  16928  pwsgsum  17009  dprd2dlem1  17090  dprd2d2  17093  ablfacrplem  17116  ablfacrp  17117  ablfacrp2  17118  ablfac1b  17121  ablfac1eu  17124  pgpfac1lem3a  17127  ablfaclem2  17137  dvdsrid  17300  dvdsrtr  17301  dvdsrneg  17303  unitmulcl  17313  unitgrp  17316  unitnegcl  17330  isdrng2  17406  subrguss  17444  subrgunit  17447  abvsubtri  17484  fidomndrnglem  17955  psrbaglesupp  18017  psrbaglesuppOLD  18018  gzrngunit  18483  prmirredlem  18523  prmirredlemOLD  18526  znidomb  18600  frlmgsum  18802  invrvald  19178  psmetsym  20814  psmettri  20815  mettri2  20844  xmetsym  20850  xmettri  20854  prdsxmetlem  20871  xblss2ps  20904  xblss2  20905  blhalf  20908  xmsge0  20966  ngptgp  21150  nrginvrcnlem  21199  nmoeq0  21243  cnmet  21279  blcvx  21303  opnreen  21336  metdcnlem  21341  metdstri  21355  metdsle  21356  metnrmlem1  21363  metnrmlem3  21365  lebnumlem1  21461  pi1inv  21552  cphnmf  21642  ipge0  21645  ipcau2  21677  tchcphlem1  21678  csbren  21826  minveclem2  21841  minveclem3  21844  ovolssnul  21898  ovolctb  21901  ovolunnul  21911  ovoliunlem1  21913  ovoliun2  21917  ovoliunnul  21918  ioombl1lem4  21971  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombl  21998  volcn  22015  vitalilem2  22018  vitalilem5  22021  itg1lea  22119  mbfi1fseqlem6  22127  mbfi1flimlem  22129  itg2eqa  22152  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2cnlem2  22169  iblabsr  22236  iblmulc2  22237  dveflem  22380  dvef  22381  dvferm2lem  22387  dvlip  22394  c1liplem1  22397  dveq0  22401  dvlt0  22406  dvivthlem1  22409  lhop1  22415  dvfsumle  22422  dvfsumlem4  22430  dvfsumrlim3  22434  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  deg1add  22504  ply1divex  22537  ply1rem  22564  fta1glem2  22567  fta1blem  22569  ig1pdvds  22577  plyeq0lem  22607  dgrcolem2  22671  plydivlem4  22692  plyrem  22701  fta1lem  22703  aalioulem3  22730  aaliou2b  22737  aaliou3lem3  22740  aaliou3lem8  22741  ulmcn  22794  ulmdvlem1  22795  itgulm  22803  pserulm  22817  pserdvlem2  22823  abelthlem2  22827  abelthlem5  22830  abelthlem6  22831  abelthlem7  22833  abelthlem8  22834  abelthlem9  22835  sinq12gt0  22900  sinq34lt0t  22902  cosq14gt0  22903  cosq14ge0  22904  efif1olem3  22931  argimgt0  22997  argimlt0  22998  logneg2  23000  logcnlem3  23025  logcnlem4  23026  logtayllem  23040  logtayl2  23043  cxpsqrtlem  23083  cxpsqrt  23084  cxpaddlelem  23125  abscxpbnd  23127  loglesqrt  23132  ang180lem2  23142  atanlogaddlem  23244  atanlogsublem  23246  atantan  23254  atans2  23262  atantayl  23268  leibpi  23273  log2tlbnd  23276  birthdaylem2  23282  birthdaylem3  23283  cxp2limlem  23305  jensenlem2  23317  jensen  23318  logdiflbnd  23324  emcllem2  23326  emcllem4  23328  harmonicbnd4  23340  fsumharmonic  23341  wilthlem3  23344  basellem1  23354  basellem3  23356  basellem4  23357  fsumdvdsdiaglem  23459  dvdsppwf1o  23462  dvdsmulf1o  23470  chteq0  23484  chtub  23487  chpub  23495  logfacubnd  23496  logfaclbnd  23497  logexprlim  23500  perfectlem2  23505  dchrfi  23530  bclbnd  23555  bposlem1  23559  bposlem3  23561  bposlem4  23562  bposlem6  23564  lgslem1  23571  lgsqrlem2  23617  lgsqrlem4  23619  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  lgsquad2lem1  23633  2sqlem3  23641  2sqlem4  23642  2sqlem8  23647  2sqlem11  23650  chebbnd1lem2  23655  chebbnd1lem3  23656  chtppilimlem1  23658  chpchtlim  23664  vmadivsum  23667  vmadivsumb  23668  rpvmasumlem  23672  dchrisumlem2  23675  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrisum0flblem2  23694  dchrisum0fno1  23696  dchrisum0re  23698  dchrisum0lem1  23701  dchrisum0lem2a  23702  mudivsum  23715  mulogsumlem  23716  mulog2sumlem2  23720  vmalogdivsum2  23723  selberglem2  23731  selbergb  23734  selberg2b  23737  logdivbnd  23741  selberg3lem1  23742  selberg3lem2  23743  selberg4lem1  23745  pntrmax  23749  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem5  23766  pntrlog2bndlem6a  23767  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem1  23774  pntibndlem2  23776  pntlemb  23782  pntlemq  23786  pntlemr  23787  pntlemj  23788  pntlemk  23791  qabvle  23810  padicabvcxp  23817  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth3  23823  legtrid  23978  legov3  23984  krippenlem  24067  mideulem2  24108  midex  24111  opphllem5  24123  opphllem6  24124  opphl  24125  lmieu  24150  lmiisolem  24161  ttgcontlem1  24188  colinearalglem4  24212  axpaschlem  24243  axcontlem7  24273  clwlkndivn  24853  nvge0  25577  smcnlem  25607  nmoub3i  25688  nmoub2i  25689  nmlno0lem  25708  minvecolem2  25791  htthlem  25834  norm3dif2  26068  bcs2  26099  chscllem2  26556  eigposi  26755  nmopub2tALT  26828  nmfnleub2  26845  nmlnop0iALT  26914  riesz1  26984  cnlnadjlem2  26987  nmopcoadji  27020  leopsq  27048  leopmul  27053  leopnmid  27057  nmopleid  27058  opsqrlem6  27064  0leopj  27105  hstle1  27145  strlem3a  27171  mdslmd4i  27252  cvexchlem  27287  cdj1i  27352  mul2lt0bi  27569  le2halvesd  27576  xlt2addrd  27578  2sqcoprm  27635  2sqmod  27636  archiabllem1a  27735  archiabllem2a  27738  archiabllem2c  27739  xrge0tsmsd  27775  orngsqr  27794  ornglmulle  27795  orngrmulle  27796  orng0le1  27802  metideq  27872  metider  27873  sqsscirc1  27890  esumle  28065  esummono  28066  esumlef  28070  esumcst  28071  aean  28216  dya2ub  28241  dya2icoseg  28248  eulerpartlemb  28307  fibp1  28340  sgnmulsgp  28489  eluzmn  28491  signsplypnf  28507  signsply0  28508  lgamgulmlem2  28572  lgamgulm2  28578  lgambdd  28579  lgamucov  28580  lgamcvglem  28582  lgamcvg2  28597  gamcvg  28598  subfacval3  28633  sconpht2  28683  sconpi1  28684  rescon  28691  snmlff  28774  sinccvglem  29038  faclimlem2  29169  btwnouttr2  29672  ltflcei  30043  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  volsupnfl  30059  dvtanlem  30064  itg2addnclem  30066  itg2addnclem3  30068  iblmulc2nc  30080  bddiblnc  30085  ftc1cnnclem  30088  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc2nc  30099  dvasin  30103  geomcau  30252  bfplem2  30319  rrncmslem  30328  rrnequiv  30331  irrapxlem1  30758  pell1qrgaplem  30809  pell1qrgap  30810  monotoddzzfi  30878  jm2.24nn  30897  congtr  30903  congmul  30905  congsub  30908  fzmaxdif  30919  acongeq  30921  bezoutr1  30924  jm2.20nn  30939  jm2.25  30941  mapfien2OLD  31042  hbtlem4  31075  dgrsub2  31084  mpaaeu  31099  idomsubgmo  31155  cvgdvgrat  31194  radcnvrat  31195  hashnzfzclim  31227  dvconstbi  31239  binomcxplemdvbinom  31258  mulltgt0  31397  oddfl  31459  2timesgt  31475  lt3addmuld  31501  lt4addmuld  31506  iccshift  31558  iooshift  31562  fsumnncl  31572  fmul01  31574  fmul01lt1lem1  31578  fmul01lt1lem2  31579  mccllem  31605  climrec  31609  climexp  31611  climneg  31616  limcrecl  31635  sumnnodd  31636  lptioo2  31637  lptioo1  31638  ltmod  31644  lptre2pt  31646  0ellimcdiv  31655  limclner  31657  cncficcgt0  31691  cncfioobdlem  31699  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvdsn1add  31736  dvnxpaek  31739  dvnmul  31740  dvnprodlem1  31743  itgiccshift  31779  itgperiod  31780  stoweidlem1  31783  stoweidlem11  31793  stoweidlem13  31795  stoweidlem26  31808  stoweidlem34  31816  stoweidlem38  31820  stoweidlem42  31824  stoweidlem51  31833  stoweidlem59  31841  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  stirlinglem13  31868  stirlinglem15  31870  dirkercncflem1  31885  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem10  31899  fourierdlem11  31900  fourierdlem15  31904  fourierdlem20  31909  fourierdlem25  31914  fourierdlem26  31915  fourierdlem30  31919  fourierdlem37  31926  fourierdlem39  31928  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem44  31933  fourierdlem47  31936  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem52  31941  fourierdlem54  31943  fourierdlem60  31949  fourierdlem61  31950  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem81  31970  fourierdlem84  31973  fourierdlem87  31976  fourierdlem92  31981  fourierdlem93  31982  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  etransclem19  32036  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem27  32044  etransclem32  32049  etransclem35  32052  etransclem48  32065  isosctrlem1ALT  33734  lsatcvatlem  34774  islshpcv  34778  atlatmstc  35044  cvlsupr7  35073  cvrval3  35137  cvrval5  35139  cvrexchlem  35143  atcvrj1  35155  cvrat3  35166  cvrat4  35167  atbtwn  35170  1cvratex  35197  hlatexch4  35205  3atlem1  35207  3atlem2  35208  atcvrlln2  35243  atcvrlln  35244  lplnllnneN  35280  llncvrlpln2  35281  4atlem3b  35322  lplncvrlvol2  35339  dalemswapyz  35380  dalemswapyzps  35414  dalem25  35422  dalem39  35435  dalem58  35454  dalem59  35455  lneq2at  35502  lncvrat  35506  dalawlem2  35596  dalawlem3  35597  dalawlem4  35598  dalawlem6  35600  dalawlem9  35603  dalawlem11  35605  dalawlem12  35606  lhpocnle  35740  lhpmcvr3  35749  lhpmcvr5N  35751  lhpmcvr6N  35752  4atexlemunv  35790  4atexlemc  35793  4atexlemex2  35795  lautm  35818  cdlemc2  35917  cdleme5  35965  cdleme11j  35992  cdleme16b  36004  cdlemednpq  36024  cdleme19e  36033  cdleme20i  36043  cdleme22a  36066  cdleme22cN  36068  cdleme22d  36069  cdleme22e  36070  cdleme22eALTN  36071  cdleme22f  36072  cdleme23c  36077  cdleme30a  36104  cdleme35a  36174  cdleme35b  36176  cdleme42h  36208  cdlemeg46rgv  36254  cdlemg8b  36354  cdlemg12e  36373  cdlemg13a  36377  cdlemg17pq  36398  cdlemg18c  36406  cdlemg19  36410  cdlemg21  36412  cdlemg31d  36426  cdlemg33a  36432  tendoid  36499  cdlemk4  36560  cdlemki  36567  cdlemk10  36569  cdlemksv2  36573  cdlemk12  36576  cdlemk14  36580  cdlemk15  36581  cdlemk1u  36585  cdlemk5u  36587  cdlemk12u  36598  cdlemk45  36673  cdlemk48  36676  dia2dimlem1  36791  dia2dimlem2  36792  dia2dimlem3  36793  cdlemm10N  36845  cdlemn2  36922  dihjustlem  36943  dihglbcpreN  37027  dihmeetlem3N  37032  int-sqgeq0d  38007  int-ineqmvtd  38012
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