Theorem breqtrd 5135

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

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	breq2d 5119	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 235	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  breqtrrd  5137  breqtrid  5146  domunsn  9128  mapdom2  9149  phplem2  9202  mapfien2  9382  wemaplem2  9522  infdifsn  9639  cantnff  9656  ttrclss  9702  rnttrcl  9704  infxpenlem  10019  infmap2  10222  ssfin4  10315  canthp1lem1  10664  nqereq  10947  ltexnq  10987  ltbtwnnq  10990  add20  11753  mullt0  11760  ltm1  12084  recgt0  12088  prodgt0  12089  ltmul1a  12091  mulge0b  12112  recp1lt1  12140  recreclt  12141  ledivp1  12144  ledivp1i  12167  ltdivp1i  12168  eluzmn  12897  ltaddrp2d  13122  mul2lt0bi  13152  prodge0rd  13153  xleadd1a  13307  xov1plusxeqvd  13553  fz01en  13609  fzonmapblen  13766  fladdz  13888  flhalf  13893  fldiv  13923  modsubdir  14006  fzen2  14035  serle  14123  ltexp2a  14232  leexp2a  14238  exple1  14243  expubnd  14244  bernneq  14295  expmulnbnd  14301  discr1  14305  discr  14306  faclbnd6  14365  hashfz  14494  hashfun  14504  seqcoll  14531  sqeqd  15255  01sqrexlem7  15337  sqrtge0  15346  sqrtneglem  15355  abslt  15404  absle  15405  abstri  15420  rlimge0  15670  reccn2  15686  climaddc2  15725  isercolllem1  15754  caucvgrlem  15762  summolem2a  15803  isumge0  15854  fsumle  15888  fsumlt  15889  o1fsum  15902  supcvg  15947  expcnv  15955  geolim  15961  geolim2  15962  georeclim  15963  geo2lim  15966  mertenslem1  15975  mertens  15977  prodmolem2a  16025  efcllem  16167  ef0lem  16168  efgt0  16195  eftlub  16201  eflt  16209  sinbnd  16272  cosbnd  16273  ef01bndlem  16276  sin01gt0  16282  cos01gt0  16283  sin02gt0  16284  eirrlem  16296  rpnnen2lem11  16316  rpnnen2lem12  16317  ruclem11  16332  dvdssub2  16395  dvdsadd2b  16400  dvdsexp  16422  3dvds  16425  opoe  16457  bitsfzolem  16528  bitsinv1lem  16535  bezoutlem4  16636  dvdsgcd  16638  dvdsmulgcd  16650  bezoutr1  16663  nn0seqcvgd  16664  rpmulgcd2  16750  qredeq  16751  rpdvds  16754  prmind2  16779  divdenle  16844  hashdvds  16870  phimullem  16874  eulerthlem2  16877  prmdiveq  16881  prmdivdiv  16882  pythagtriplem4  16915  pythagtriplem10  16916  pythagtriplem19  16929  iserodd  16931  pcpre1  16938  pcadd2  16986  qexpz  16997  expnprm  16998  oddprmdvds  16999  pockthlem  17001  prmreclem2  17013  prmreclem3  17014  4sqlem7  17040  4sqlem10  17043  4sqlem11  17051  4sqlem12  17052  4sqlem14  17054  4sqlem15  17055  4sqlem16  17056  0ram  17116  ffthiso  18024  latmlej12  18571  qusgrp  19315  pgpfi1  19723  sylow1lem4  19729  sylow1lem5  19730  odcau  19732  pgpfi  19733  pgpssslw  19742  sylow3lem4  19758  sylow3lem6  19760  efgsfo  19867  frgp0  19888  odadd1  19976  odadd2  19977  odadd  19978  gexexlem  19980  lt6abl  20023  gsumzsubmcl  20046  pwsgsum  20110  dprd2dlem1  20171  dprd2d2  20174  ablfacrplem  20195  ablfacrp  20196  ablfacrp2  20197  ablfac1b  20200  ablfac1eu  20203  pgpfac1lem3a  20206  ablfaclem2  20216  dvdsrid  20509  dvdsrtr  20510  dvdsrneg  20512  unitmulcl  20522  unitgrp  20525  unitnegcl  20539  subrguss  20750  subrgunit  20753  isdrng2  20907  fidomndrnglem  20940  abvsubtri  20994  orngsqr  21033  ornglmulle  21034  orngrmulle  21035  orng0le1  21041  gzrngunit  21647  prmirredlem  21686  znidomb  21775  frlmgsum  21986  psrbaglesupp  22138  psdmul  22395  psdmvr  22398  invrvald  22899  psmetsym  24537  psmettri  24538  mettri2  24568  xmetsym  24574  xmettri  24578  prdsxmetlem  24595  xblss2ps  24628  xblss2  24629  blhalf  24632  xmsge0  24690  ngptgp  24863  nrginvrcnlem  24918  nmoeq0  24963  cnmet  24998  blcvx  25025  opnreen  25059  metdcnlem  25064  metdstri  25079  metdsle  25080  metnrmlem1  25087  metnrmlem3  25089  lebnumlem1  25190  pi1inv  25281  cphnmf  25424  ipge0  25427  ipcau2  25463  tcphcphlem1  25464  csbren  25628  minveclem2  25655  minveclem3  25658  ovolssnul  25716  ovolctb  25719  ovolunnul  25729  ovoliunlem1  25731  ovoliun2  25735  ovoliunnul  25736  ioombl1lem4  25790  uniioombllem3  25814  uniioombllem4  25815  uniioombllem5  25816  uniioombl  25818  volcn  25835  vitalilem2  25838  vitalilem5  25841  itg1lea  25941  mbfi1fseqlem6  25949  mbfi1flimlem  25951  itg2eqa  25974  itg2splitlem  25977  itg2split  25978  itg2monolem1  25979  itg2cnlem2  25991  iblabsr  26059  iblmulc2  26060  bddiblnc  26071  dveflem  26208  dvef  26209  dvferm2lem  26215  dvlip  26222  c1liplem1  26225  dveq0  26229  dvlt0  26234  dvivthlem1  26237  lhop1  26243  dvfsumle  26250  dvfsumlem4  26258  dvfsumrlim3  26262  dvfsum2  26263  ftc1a  26266  ftc1lem4  26268  deg1add  26330  ply1divex  26364  ply1rem  26393  fta1glem2  26396  fta1blem  26398  ig1pdvds  26407  plyeq0lem  26437  dgrcolem2  26501  plydivlem4  26527  plyrem  26536  fta1lem  26538  aalioulem3  26567  aaliou2b  26574  aaliou3lem3  26577  aaliou3lem8  26578  ulmcn  26632  ulmdvlem1  26633  itgulm  26641  pserulm  26655  pserdvlem2  26661  abelthlem2  26665  abelthlem5  26668  abelthlem6  26669  abelthlem7  26671  abelthlem8  26672  abelthlem9  26673  sinq12gt0  26742  sinq34lt0t  26744  cosq14gt0  26745  cosq14ge0  26746  cos02pilt1  26761  efif1olem3  26779  argimgt0  26847  argimlt0  26848  logneg2  26850  logcnlem3  26879  logcnlem4  26880  logtayllem  26894  logtayl2  26897  cxpsqrtlem  26937  cxpsqrt  26938  cxpaddlelem  26986  abscxpbnd  26988  zrtdvds  26994  rtprmirr  26995  loglesqrt  26996  ang180lem2  27045  atanlogaddlem  27148  atanlogsublem  27150  atantan  27158  atans2  27166  atantayl  27172  leibpi  27177  log2tlbnd  27180  birthdaylem2  27187  birthdaylem3  27188  cxp2limlem  27210  jensenlem2  27222  jensen  27223  logdiflbnd  27229  emcllem2  27231  emcllem4  27233  harmonicbnd4  27245  fsumharmonic  27246  lgamgulmlem2  27264  lgamgulm2  27270  lgambdd  27271  lgamucov  27272  lgamcvglem  27274  lgamcvg2  27289  gamcvg  27290  wilthlem3  27304  basellem1  27315  basellem3  27317  basellem4  27318  fsumdvdsdiaglem  27417  dvdsppwf1o  27420  mpodvdsmulf1o  27428  dvdsmulf1o  27430  chteq0  27443  chtub  27446  chpub  27454  logfacubnd  27455  logfaclbnd  27456  logexprlim  27459  perfectlem2  27464  dchrfi  27489  bclbnd  27514  bposlem1  27518  bposlem3  27520  bposlem4  27521  bposlem6  27523  lgslem1  27531  lgsqrlem2  27581  lgsqrlem4  27583  lgseisenlem2  27610  lgsquadlem1  27614  lgsquadlem2  27615  lgsquad2lem1  27618  2sqlem3  27654  2sqlem4  27655  2sqlem8  27660  2sqlem11  27663  2sqcoprm  27669  2sqmod  27670  chebbnd1lem2  27704  chebbnd1lem3  27705  chtppilimlem1  27707  chpchtlim  27713  vmadivsum  27716  vmadivsumb  27717  rpvmasumlem  27721  dchrisumlem2  27724  dchrmusum2  27728  dchrvmasumlem2  27732  dchrvmasumlem3  27733  dchrisum0flblem2  27743  dchrisum0fno1  27745  dchrisum0re  27747  dchrisum0lem1  27750  dchrisum0lem2a  27751  mudivsum  27764  mulogsumlem  27765  mulog2sumlem2  27769  vmalogdivsum2  27772  selberglem2  27780  selbergb  27783  selberg2b  27786  logdivbnd  27790  selberg3lem1  27791  selberg3lem2  27792  selberg4lem1  27794  pntrmax  27798  pntrlog2bndlem2  27812  pntrlog2bndlem3  27813  pntrlog2bndlem5  27815  pntrlog2bndlem6a  27816  pntrlog2bndlem6  27817  pntrlog2bnd  27818  pntpbnd1a  27819  pntpbnd1  27820  pntpbnd2  27821  pntibndlem1  27823  pntibndlem2  27825  pntlemb  27831  pntlemq  27835  pntlemr  27836  pntlemj  27837  pntlemk  27840  qabvle  27859  padicabvcxp  27866  ostth2lem2  27868  ostth2lem3  27869  ostth2lem4  27870  ostth3  27872  addsuniflem  28264  negsid  28304  negsunif  28318  negright  28322  mulsuniflem  28412  ltmuls2  28434  precsexlem9  28478  absmuls  28507  zcuts  28670  addhalfcut  28722  pw2cut2  28725  bdayfinbndlem1  28730  z12sge0  28746  legtrid  28931  legov3  28938  krippenlem  29039  mideulem2  29087  midex  29090  opphllem5  29104  opphllem6  29105  opphl  29107  lmieu  29166  lmiisolem  29178  perpeqlem  29224  angmndaddcpbl  29263  prlnghpg  29289  perpprlng  29293  prlngsymquadlem  29306  quadcgrprlng  29309  tgaltai  29310  ttgcontlem1  29327  colinearalglem4  29352  axpaschlem  29383  axcontlem7  29413  nbfusgrlevtxm2  29824  clwlksndivn  30542  eucrct2eupth  30711  nvge0  31140  smcnlem  31164  nmoub3i  31240  nmoub2i  31241  nmlno0lem  31260  minvecolem2  31342  htthlem  31384  norm3dif2  31618  bcs2  31649  chscllem2  32105  eigposi  32303  nmopub2tALT  32376  nmfnleub2  32393  nmlnop0iALT  32462  riesz1  32532  cnlnadjlem2  32535  nmopcoadji  32568  leopsq  32596  leopmul  32601  leopnmid  32605  nmopleid  32606  opsqrlem6  32612  0leopj  32653  hstle1  32693  strlem3a  32719  mdslmd4i  32800  cvexchlem  32835  cdj1i  32900  unidifsnel  32996  unidifsnne  32997  le2halvesd  33214  xlt2addrd  33217  fsumub  33285  sgnmulsgp  33289  2exple2exp  33291  oexpled  33293  wrdt2ind  33382  xrge0tsmsd  33500  fzto1st1  33529  cycpmco2lem4  33556  cycpmco2lem6  33558  cyc3conja  33584  archiabllem1a  33618  archiabllem2a  33621  archiabllem2c  33622  rprmdvdsprod  33931  1arithidomlem1  33932  1arithidomlem2  33933  1arithidom  33934  ply1dg3rt0irred  33981  mplmulmvr  34036  mplvrpmrhm  34044  exsslsb  34094  fedgmullem1  34126  fedgmullem2  34127  fldsdrgfldext2  34159  fldextrspundgdvdslem  34177  fldextrspundgdvds  34178  fldext2rspun  34179  extdgfialglem2  34190  algextdeglem8  34221  rtelextdg2lem  34223  constrext2chnlem  34247  cos9thpiminplylem1  34279  cos9thpiminplylem2  34280  metideq  34390  metider  34391  sqsscirc1  34405  esummono  34551  esumpad2  34553  esumle  34555  esumlef  34559  esumcst  34560  esumrnmpt2  34565  esum2d  34590  aean  34742  dya2ub  34768  dya2icoseg  34775  omssubadd  34798  inelcarsg  34809  carsgsigalem  34813  carsggect  34816  carsgclctunlem2  34817  eulerpartlemb  34866  fibp1  34899  signsplypnf  35045  signsply0  35046  fdvposlt  35094  fdvposle  35096  reprgt  35116  logdivsqrle  35145  hgt750lemb  35151  hgt750leme  35153  tgoldbachgtde  35155  subfacval3  35755  sconnpht2  35804  sconnpi1  35805  resconn  35812  snmlff  35895  sinccvglem  36238  faclimlem2  36310  btwnouttr2  36589  weiunpo  37071  dnibndlem5  37166  dnibndlem7  37168  dnibndlem8  37169  dnibndlem9  37170  dnibndlem10  37171  dnibnd  37175  knoppcnlem4  37180  knoppcnlem9  37185  unbdqndv2lem1  37193  unbdqndv2lem2  37194  knoppndvlem11  37206  knoppndvlem12  37207  knoppndvlem14  37209  knoppndvlem15  37210  knoppndvlem17  37212  knoppndvlem18  37213  knoppndvlem19  37214  knoppndvlem21  37216  ltflcei  38349  poimirlem9  38365  poimirlem26  38382  poimirlem27  38383  poimirlem29  38385  heicant  38391  mblfinlem2  38394  mblfinlem3  38395  mblfinlem4  38396  volsupnfl  38401  itg2addnclem  38407  itg2addnclem3  38409  iblmulc2nc  38421  ftc1cnnclem  38427  ftc1anclem6  38434  ftc1anclem7  38435  ftc1anclem8  38436  ftc2nc  38438  dvasin  38440  geomcau  38496  bfplem2  38560  rrncmslem  38569  rrnequiv  38572  lsatcvatlem  39909  islshpcv  39913  atlatmstc  40179  cvlsupr7  40208  cvrval3  40273  cvrval5  40275  cvrexchlem  40279  atcvrj1  40291  cvrat3  40302  cvrat4  40303  atbtwn  40306  1cvratex  40333  hlatexch4  40341  3atlem1  40343  3atlem2  40344  atcvrlln2  40379  atcvrlln  40380  lplnllnneN  40416  llncvrlpln2  40417  4atlem3b  40458  lplncvrlvol2  40475  dalemswapyz  40516  dalemswapyzps  40550  dalem25  40558  dalem39  40571  dalem58  40590  dalem59  40591  lneq2at  40638  lncvrat  40642  dalawlem2  40732  dalawlem3  40733  dalawlem4  40734  dalawlem6  40736  dalawlem9  40739  dalawlem11  40741  dalawlem12  40742  lhpocnle  40876  lhpmcvr3  40885  lhpmcvr5N  40887  lhpmcvr6N  40888  4atexlemunv  40926  4atexlemc  40929  4atexlemex2  40931  lautm  40954  cdlemc2  41052  cdleme5  41100  cdleme11j  41127  cdleme16b  41139  cdlemednpq  41159  cdleme19e  41167  cdleme20i  41177  cdleme22a  41200  cdleme22cN  41202  cdleme22d  41203  cdleme22e  41204  cdleme22eALTN  41205  cdleme22f  41206  cdleme23c  41211  cdleme30a  41238  cdleme35a  41308  cdleme35b  41310  cdleme42h  41342  cdlemeg46rgv  41388  cdlemg8b  41488  cdlemg12e  41507  cdlemg13a  41511  cdlemg17pq  41532  cdlemg18c  41540  cdlemg19  41544  cdlemg21  41546  cdlemg31d  41560  cdlemg33a  41566  tendoid  41633  cdlemk4  41694  cdlemki  41701  cdlemk10  41703  cdlemksv2  41707  cdlemk12  41710  cdlemk14  41714  cdlemk15  41715  cdlemk1u  41719  cdlemk5u  41721  cdlemk12u  41732  cdlemk45  41807  cdlemk48  41810  dia2dimlem1  41924  dia2dimlem2  41925  dia2dimlem3  41926  cdlemm10N  41978  cdlemn2  42055  dihjustlem  42076  dihglbcpreN  42160  dihmeetlem3N  42165  nnproddivdvdsd  42853  lcmineqlem17  42898  lcmineqlem18  42899  3lexlogpow2ineq1  42911  3lexlogpow2ineq2  42912  3lexlogpow5ineq5  42913  aks4d1p1p3  42922  aks4d1p1p2  42923  aks4d1p1p4  42924  aks4d1p1p5  42928  aks4d1p1  42929  aks4d1p3  42931  aks4d1p8  42940  posbezout  42953  primrootspoweq0  42959  aks6d1c1  42969  hashscontpow1  42974  aks6d1c4  42977  aks6d1c2  42983  aks6d1c5lem1  42989  aks6d1c5lem3  42990  aks6d1c5lem2  42991  deg1gprod  42993  sticksstones7  43005  sticksstones10  43008  sticksstones12  43011  sticksstones22  43021  aks6d1c6lem1  43023  aks6d1c6lem3  43025  aks6d1c6lem4  43026  bcled  43031  bcle2d  43032  aks6d1c7lem1  43033  unitscyglem4  43051  aks5lem7  43053  aks5  43057  explt1d  43185  mulgt0b2d  43353  evlselv  43422  dffltz  43467  fltdvdsabdvdsc  43471  fltaccoprm  43473  fltabcoprm  43475  flt4lem5elem  43484  flt4lem7  43492  fltnlta  43496  irrapxlem1  43650  pell1qrgaplem  43701  pell1qrgap  43702  monotoddzzfi  43770  jm2.24nn  43787  congtr  43793  congmul  43795  congsub  43798  fzmaxdif  43809  acongeq  43811  jm2.20nn  43825  jm2.25  43827  hbtlem4  43954  dgrsub2  43963  mpaaeu  43978  idomsubgmo  44021  iscard4  44360  sqrtcvallem4  44466  leeq2d  44985  int-sqgeq0d  45013  int-ineqmvtd  45018  cvgdvgrat  45124  radcnvrat  45125  hashnzfzclim  45133  dvconstbi  45145  binomcxplemdvbinom  45164  isosctrlem1ALT  45743  mulltgt0  45843  rnmptbd2lem  46064  oddfl  46098  2timesgt  46108  lt3addmuld  46121  lt4addmuld  46126  supxrgere  46150  supxrgelem  46154  supxrge  46155  xadd0ge2  46158  infrpge  46168  xrlexaddrp  46169  xralrple2  46171  infxr  46183  infleinflem1  46186  infleinflem2  46187  infleinf  46188  xralrple4  46189  xralrple3  46190  recnnltrp  46193  rpgtrecnn  46196  xrralrecnnge  46206  rexabslelem  46233  infrnmptle  46238  supminfxr  46279  xrpnf  46300  iccshift  46335  iooshift  46339  ressiocsup  46371  ressioosup  46372  fsumnncl  46389  fmul01  46397  fmul01lt1lem1  46401  fmul01lt1lem2  46402  mccllem  46414  climrec  46420  climexp  46422  climneg  46427  limcrecl  46446  sumnnodd  46447  lptioo2  46448  lptioo1  46449  ltmod  46453  lptre2pt  46455  0ellimcdiv  46464  limclner  46466  fnlimcnv  46482  climinf2lem  46521  limsupubuzlem  46527  limsup10exlem  46587  limsupgtlem  46592  dfxlim2v  46662  xlimliminflimsup  46677  cncficcgt0  46703  cncfioobdlem  46711  ioodvbdlimc1lem1  46746  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  dvdsn1add  46754  dvnxpaek  46757  dvnmul  46758  dvnprodlem1  46761  itgiccshift  46795  itgperiod  46796  sublevolico  46799  ismbl3  46801  ovolsplit  46803  ismbl4  46808  stoweidlem1  46816  stoweidlem11  46826  stoweidlem13  46828  stoweidlem26  46841  stoweidlem34  46849  stoweidlem38  46853  stoweidlem42  46857  stoweidlem51  46866  stoweidlem59  46874  stirlinglem5  46893  stirlinglem6  46894  stirlinglem7  46895  stirlinglem10  46898  stirlinglem11  46899  stirlinglem13  46901  stirlinglem15  46903  dirkercncflem1  46918  dirkercncflem4  46921  fourierdlem4  46926  fourierdlem10  46932  fourierdlem11  46933  fourierdlem15  46937  fourierdlem20  46942  fourierdlem25  46947  fourierdlem26  46948  fourierdlem30  46952  fourierdlem37  46959  fourierdlem39  46961  fourierdlem40  46962  fourierdlem41  46963  fourierdlem42  46964  fourierdlem44  46966  fourierdlem47  46968  fourierdlem48  46969  fourierdlem49  46970  fourierdlem50  46971  fourierdlem51  46972  fourierdlem52  46973  fourierdlem54  46975  fourierdlem60  46981  fourierdlem61  46982  fourierdlem63  46984  fourierdlem64  46985  fourierdlem65  46986  fourierdlem73  46994  fourierdlem74  46995  fourierdlem75  46996  fourierdlem76  46997  fourierdlem78  46999  fourierdlem79  47000  fourierdlem81  47002  fourierdlem84  47005  fourierdlem87  47008  fourierdlem92  47013  fourierdlem93  47014  fourierdlem101  47022  fourierdlem102  47023  fourierdlem103  47024  fourierdlem104  47025  fourierdlem111  47032  fourierdlem114  47035  sqwvfoura  47043  sqwvfourb  47044  fouriersw  47046  etransclem19  47068  etransclem23  47072  etransclem24  47073  etransclem25  47074  etransclem27  47076  etransclem32  47081  etransclem35  47084  etransclem48  47097  qndenserrnbllem  47109  ioorrnopnlem  47119  ioorrnopnxrlem  47121  fsumlesge0  47192  sge0cl  47196  sge0supre  47204  sge0less  47207  sge0gerp  47210  sge0ltfirp  47215  sge0le  47222  sge0ltfirpmpt  47223  sge0split  47224  sge0rpcpnf  47236  sge0ltfirpmpt2  47241  sge0isum  47242  sge0xaddlem1  47248  sge0pnffigtmpt  47255  sge0pnffsumgt  47257  sge0gtfsumgt  47258  sge0seq  47261  nnfoctbdjlem  47270  meassle  47278  meaiuninclem  47295  meaiininclem  47301  omeiunle  47332  omeiunltfirp  47334  carageniuncllem2  47337  carageniuncl  47338  omess0  47349  hoicvr  47363  ovnlerp  47377  ovnsubaddlem1  47385  hsphoidmvle2  47400  hoidmv1lelem2  47407  hoidmv1le  47409  hoidmvlelem1  47410  hoidmvlelem2  47411  hoidmvlelem3  47412  hoidmvlelem5  47414  ovnhoilem2  47417  ovnhoi  47418  hoidifhspdmvle  47435  hoiqssbllem2  47438  hspmbllem2  47442  hspmbllem3  47443  hspmbl  47444  vonioolem2  47496  vonicclem2  47499  smfaddlem1  47578  smflimlem2  47587  smflimlem4  47589  smfmullem1  47606  smfinflem  47632  smflimsuplem4  47638  smflimsuplem8  47642  chnsubseq  47695  sqrtnpoly  47748  perfectALTVlem2  48625  nnpw2blen  49497  itscnhlinecirc02plem1  49699  funcoppc3  50060  oppcuprcl2  50115  isinito3  50413