Theorem breqtrd 5115

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 5101	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  breqtrrd  5117  breqtrid  5126  domunsn  9040  mapdom2  9061  phplem2  9114  mapfien2  9293  wemaplem2  9433  infdifsn  9547  cantnff  9564  ttrclss  9610  rnttrcl  9612  infxpenlem  9904  infmap2  10108  ssfin4  10201  canthp1lem1  10543  nqereq  10826  ltexnq  10866  ltbtwnnq  10869  add20  11629  mullt0  11636  ltm1  11963  recgt0  11967  prodgt0  11968  ltmul1a  11970  mulge0b  11992  recp1lt1  12020  recreclt  12021  ledivp1  12024  ledivp1i  12047  ltdivp1i  12048  eluzmn  12739  ltaddrp2d  12968  mul2lt0bi  12998  prodge0rd  12999  xleadd1a  13152  xov1plusxeqvd  13398  fz01en  13452  fzonmapblen  13608  fladdz  13729  flhalf  13734  fldiv  13764  modsubdir  13847  fzen2  13876  serle  13964  ltexp2a  14073  leexp2a  14079  exple1  14084  expubnd  14085  bernneq  14136  expmulnbnd  14142  discr1  14146  discr  14147  faclbnd6  14206  hashfz  14334  hashfun  14344  seqcoll  14371  sqeqd  15073  01sqrexlem7  15155  sqrtge0  15164  sqrtneglem  15173  abslt  15222  absle  15223  abstri  15238  rlimge0  15488  reccn2  15504  climaddc2  15543  isercolllem1  15572  caucvgrlem  15580  summolem2a  15622  isumge0  15673  fsumle  15706  fsumlt  15707  o1fsum  15720  supcvg  15763  expcnv  15771  geolim  15777  geolim2  15778  georeclim  15779  geo2lim  15782  mertenslem1  15791  mertens  15793  prodmolem2a  15841  efcllem  15984  ef0lem  15985  efgt0  16012  eftlub  16018  eflt  16026  sinbnd  16089  cosbnd  16090  ef01bndlem  16093  sin01gt0  16099  cos01gt0  16100  sin02gt0  16101  eirrlem  16113  rpnnen2lem11  16133  rpnnen2lem12  16134  ruclem11  16149  dvdssub2  16212  dvdsadd2b  16217  dvdsexp  16239  3dvds  16242  opoe  16274  bitsfzolem  16345  bitsinv1lem  16352  bezoutlem4  16453  dvdsgcd  16455  dvdsmulgcd  16467  bezoutr1  16480  nn0seqcvgd  16481  rpmulgcd2  16567  qredeq  16568  rpdvds  16571  prmind2  16596  divdenle  16660  hashdvds  16686  phimullem  16690  eulerthlem2  16693  prmdiveq  16697  prmdivdiv  16698  pythagtriplem4  16731  pythagtriplem10  16732  pythagtriplem19  16745  iserodd  16747  pcpre1  16754  pcadd2  16802  qexpz  16813  expnprm  16814  oddprmdvds  16815  pockthlem  16817  prmreclem2  16829  prmreclem3  16830  4sqlem7  16856  4sqlem10  16859  4sqlem11  16867  4sqlem12  16868  4sqlem14  16870  4sqlem15  16871  4sqlem16  16872  0ram  16932  ffthiso  17838  latmlej12  18385  qusgrp  19098  pgpfi1  19507  sylow1lem4  19513  sylow1lem5  19514  odcau  19516  pgpfi  19517  pgpssslw  19526  sylow3lem4  19542  sylow3lem6  19544  efgsfo  19651  frgp0  19672  odadd1  19760  odadd2  19761  odadd  19762  gexexlem  19764  lt6abl  19807  gsumzsubmcl  19830  pwsgsum  19894  dprd2dlem1  19955  dprd2d2  19958  ablfacrplem  19979  ablfacrp  19980  ablfacrp2  19981  ablfac1b  19984  ablfac1eu  19987  pgpfac1lem3a  19990  ablfaclem2  20000  dvdsrid  20285  dvdsrtr  20286  dvdsrneg  20288  unitmulcl  20298  unitgrp  20301  unitnegcl  20315  subrguss  20502  subrgunit  20505  isdrng2  20658  fidomndrnglem  20687  abvsubtri  20742  orngsqr  20781  ornglmulle  20782  orngrmulle  20783  orng0le1  20789  gzrngunit  21370  prmirredlem  21409  znidomb  21498  frlmgsum  21709  psrbaglesupp  21859  psdmul  22081  psdmvr  22084  invrvald  22591  psmetsym  24225  psmettri  24226  mettri2  24256  xmetsym  24262  xmettri  24266  prdsxmetlem  24283  xblss2ps  24316  xblss2  24317  blhalf  24320  xmsge0  24378  ngptgp  24551  nrginvrcnlem  24606  nmoeq0  24651  cnmet  24686  blcvx  24713  opnreen  24747  metdcnlem  24752  metdstri  24767  metdsle  24768  metnrmlem1  24775  metnrmlem3  24777  lebnumlem1  24887  pi1inv  24979  cphnmf  25122  ipge0  25125  ipcau2  25161  tcphcphlem1  25162  csbren  25326  minveclem2  25353  minveclem3  25356  ovolssnul  25415  ovolctb  25418  ovolunnul  25428  ovoliunlem1  25430  ovoliun2  25434  ovoliunnul  25435  ioombl1lem4  25489  uniioombllem3  25513  uniioombllem4  25514  uniioombllem5  25515  uniioombl  25517  volcn  25534  vitalilem2  25537  vitalilem5  25540  itg1lea  25640  mbfi1fseqlem6  25648  mbfi1flimlem  25650  itg2eqa  25673  itg2splitlem  25676  itg2split  25677  itg2monolem1  25678  itg2cnlem2  25690  iblabsr  25758  iblmulc2  25759  bddiblnc  25770  dveflem  25910  dvef  25911  dvferm2lem  25917  dvlip  25925  c1liplem1  25928  dveq0  25932  dvlt0  25937  dvivthlem1  25940  lhop1  25946  dvfsumle  25953  dvfsumleOLD  25954  dvfsumlem4  25963  dvfsumrlim3  25967  dvfsum2  25968  ftc1a  25971  ftc1lem4  25973  deg1add  26035  ply1divex  26069  ply1rem  26098  fta1glem2  26101  fta1blem  26103  ig1pdvds  26112  plyeq0lem  26142  dgrcolem2  26207  plydivlem4  26231  plyrem  26240  fta1lem  26242  aalioulem3  26269  aaliou2b  26276  aaliou3lem3  26279  aaliou3lem8  26280  ulmcn  26335  ulmdvlem1  26336  itgulm  26344  pserulm  26358  pserdvlem2  26365  abelthlem2  26369  abelthlem5  26372  abelthlem6  26373  abelthlem7  26375  abelthlem8  26376  abelthlem9  26377  sinq12gt0  26443  sinq34lt0t  26445  cosq14gt0  26446  cosq14ge0  26447  cos02pilt1  26462  efif1olem3  26480  argimgt0  26548  argimlt0  26549  logneg2  26551  logcnlem3  26580  logcnlem4  26581  logtayllem  26595  logtayl2  26598  cxpsqrtlem  26638  cxpsqrt  26639  cxpaddlelem  26688  abscxpbnd  26690  zrtdvds  26696  rtprmirr  26697  loglesqrt  26698  ang180lem2  26747  atanlogaddlem  26850  atanlogsublem  26852  atantan  26860  atans2  26868  atantayl  26874  leibpi  26879  log2tlbnd  26882  birthdaylem2  26889  birthdaylem3  26890  cxp2limlem  26913  jensenlem2  26925  jensen  26926  logdiflbnd  26932  emcllem2  26934  emcllem4  26936  harmonicbnd4  26948  fsumharmonic  26949  lgamgulmlem2  26967  lgamgulm2  26973  lgambdd  26974  lgamucov  26975  lgamcvglem  26977  lgamcvg2  26992  gamcvg  26993  wilthlem3  27007  basellem1  27018  basellem3  27020  basellem4  27021  fsumdvdsdiaglem  27120  dvdsppwf1o  27123  mpodvdsmulf1o  27131  dvdsmulf1o  27133  chteq0  27147  chtub  27150  chpub  27158  logfacubnd  27159  logfaclbnd  27160  logexprlim  27163  perfectlem2  27168  dchrfi  27193  bclbnd  27218  bposlem1  27222  bposlem3  27224  bposlem4  27225  bposlem6  27227  lgslem1  27235  lgsqrlem2  27285  lgsqrlem4  27287  lgseisenlem2  27314  lgsquadlem1  27318  lgsquadlem2  27319  lgsquad2lem1  27322  2sqlem3  27358  2sqlem4  27359  2sqlem8  27364  2sqlem11  27367  2sqcoprm  27373  2sqmod  27374  chebbnd1lem2  27408  chebbnd1lem3  27409  chtppilimlem1  27411  chpchtlim  27417  vmadivsum  27420  vmadivsumb  27421  rpvmasumlem  27425  dchrisumlem2  27428  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumlem3  27437  dchrisum0flblem2  27447  dchrisum0fno1  27449  dchrisum0re  27451  dchrisum0lem1  27454  dchrisum0lem2a  27455  mudivsum  27468  mulogsumlem  27469  mulog2sumlem2  27473  vmalogdivsum2  27476  selberglem2  27484  selbergb  27487  selberg2b  27490  logdivbnd  27494  selberg3lem1  27495  selberg3lem2  27496  selberg4lem1  27498  pntrmax  27502  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem5  27519  pntrlog2bndlem6a  27520  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem1  27527  pntibndlem2  27529  pntlemb  27535  pntlemq  27539  pntlemr  27540  pntlemj  27541  pntlemk  27544  qabvle  27563  padicabvcxp  27570  ostth2lem2  27572  ostth2lem3  27573  ostth2lem4  27574  ostth3  27576  addsuniflem  27944  negsid  27983  negsunif  27997  mulsuniflem  28088  sltmul2  28110  precsexlem9  28153  absmuls  28182  zscut  28331  addhalfcut  28379  pw2cut2  28382  zs12ge0  28393  legtrid  28569  legov3  28576  krippenlem  28668  mideulem2  28712  midex  28715  opphllem5  28729  opphllem6  28730  opphl  28732  lmieu  28762  lmiisolem  28774  ttgcontlem1  28863  colinearalglem4  28887  axpaschlem  28918  axcontlem7  28948  nbfusgrlevtxm2  29356  clwlksndivn  30066  eucrct2eupth  30225  nvge0  30653  smcnlem  30677  nmoub3i  30753  nmoub2i  30754  nmlno0lem  30773  minvecolem2  30855  htthlem  30897  norm3dif2  31131  bcs2  31162  chscllem2  31618  eigposi  31816  nmopub2tALT  31889  nmfnleub2  31906  nmlnop0iALT  31975  riesz1  32045  cnlnadjlem2  32048  nmopcoadji  32081  leopsq  32109  leopmul  32114  leopnmid  32118  nmopleid  32119  opsqrlem6  32125  0leopj  32166  hstle1  32206  strlem3a  32232  mdslmd4i  32313  cvexchlem  32348  cdj1i  32413  unidifsnel  32515  unidifsnne  32516  le2halvesd  32739  xlt2addrd  32742  fsumub  32811  sgnmulsgp  32826  2exple2exp  32828  oexpled  32830  wrdt2ind  32934  xrge0tsmsd  33042  fzto1st1  33071  cycpmco2lem4  33098  cycpmco2lem6  33100  cyc3conja  33126  archiabllem1a  33160  archiabllem2a  33163  archiabllem2c  33164  rprmdvdsprod  33499  1arithidomlem1  33500  1arithidomlem2  33501  1arithidom  33502  ply1dg3rt0irred  33546  mplvrpmrhm  33577  exsslsb  33609  fedgmullem1  33642  fedgmullem2  33643  fldsdrgfldext2  33675  fldextrspundgdvdslem  33693  fldextrspundgdvds  33694  fldext2rspun  33695  extdgfialglem2  33706  algextdeglem8  33737  rtelextdg2lem  33739  constrext2chnlem  33763  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  metideq  33906  metider  33907  sqsscirc1  33921  esummono  34067  esumpad2  34069  esumle  34071  esumlef  34075  esumcst  34076  esumrnmpt2  34081  esum2d  34106  aean  34257  dya2ub  34283  dya2icoseg  34290  omssubadd  34313  inelcarsg  34324  carsgsigalem  34328  carsggect  34331  carsgclctunlem2  34332  eulerpartlemb  34381  fibp1  34414  signsplypnf  34563  signsply0  34564  fdvposlt  34612  fdvposle  34614  reprgt  34634  logdivsqrle  34663  hgt750lemb  34669  hgt750leme  34671  tgoldbachgtde  34673  subfacval3  35233  sconnpht2  35282  sconnpi1  35283  resconn  35290  snmlff  35373  sinccvglem  35716  faclimlem2  35788  btwnouttr2  36066  weiunpo  36509  dnibndlem5  36526  dnibndlem7  36528  dnibndlem8  36529  dnibndlem9  36530  dnibndlem10  36531  dnibnd  36535  knoppcnlem4  36540  knoppcnlem9  36545  unbdqndv2lem1  36553  unbdqndv2lem2  36554  knoppndvlem11  36566  knoppndvlem12  36567  knoppndvlem14  36569  knoppndvlem15  36570  knoppndvlem17  36572  knoppndvlem18  36573  knoppndvlem19  36574  knoppndvlem21  36576  ltflcei  37647  poimirlem9  37668  poimirlem26  37685  poimirlem27  37686  poimirlem29  37688  heicant  37694  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  volsupnfl  37704  itg2addnclem  37710  itg2addnclem3  37712  iblmulc2nc  37724  ftc1cnnclem  37730  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc2nc  37741  dvasin  37743  geomcau  37798  bfplem2  37862  rrncmslem  37871  rrnequiv  37874  lsatcvatlem  39147  islshpcv  39151  atlatmstc  39417  cvlsupr7  39446  cvrval3  39511  cvrval5  39513  cvrexchlem  39517  atcvrj1  39529  cvrat3  39540  cvrat4  39541  atbtwn  39544  1cvratex  39571  hlatexch4  39579  3atlem1  39581  3atlem2  39582  atcvrlln2  39617  atcvrlln  39618  lplnllnneN  39654  llncvrlpln2  39655  4atlem3b  39696  lplncvrlvol2  39713  dalemswapyz  39754  dalemswapyzps  39788  dalem25  39796  dalem39  39809  dalem58  39828  dalem59  39829  lneq2at  39876  lncvrat  39880  dalawlem2  39970  dalawlem3  39971  dalawlem4  39972  dalawlem6  39974  dalawlem9  39977  dalawlem11  39979  dalawlem12  39980  lhpocnle  40114  lhpmcvr3  40123  lhpmcvr5N  40125  lhpmcvr6N  40126  4atexlemunv  40164  4atexlemc  40167  4atexlemex2  40169  lautm  40192  cdlemc2  40290  cdleme5  40338  cdleme11j  40365  cdleme16b  40377  cdlemednpq  40397  cdleme19e  40405  cdleme20i  40415  cdleme22a  40438  cdleme22cN  40440  cdleme22d  40441  cdleme22e  40442  cdleme22eALTN  40443  cdleme22f  40444  cdleme23c  40449  cdleme30a  40476  cdleme35a  40546  cdleme35b  40548  cdleme42h  40580  cdlemeg46rgv  40626  cdlemg8b  40726  cdlemg12e  40745  cdlemg13a  40749  cdlemg17pq  40770  cdlemg18c  40778  cdlemg19  40782  cdlemg21  40784  cdlemg31d  40798  cdlemg33a  40804  tendoid  40871  cdlemk4  40932  cdlemki  40939  cdlemk10  40941  cdlemksv2  40945  cdlemk12  40948  cdlemk14  40952  cdlemk15  40953  cdlemk1u  40957  cdlemk5u  40959  cdlemk12u  40970  cdlemk45  41045  cdlemk48  41048  dia2dimlem1  41162  dia2dimlem2  41163  dia2dimlem3  41164  cdlemm10N  41216  cdlemn2  41293  dihjustlem  41314  dihglbcpreN  41398  dihmeetlem3N  41403  nnproddivdvdsd  42092  lcmineqlem17  42137  lcmineqlem18  42138  3lexlogpow2ineq1  42150  3lexlogpow2ineq2  42151  3lexlogpow5ineq5  42152  aks4d1p1p3  42161  aks4d1p1p2  42162  aks4d1p1p4  42163  aks4d1p1p5  42167  aks4d1p1  42168  aks4d1p3  42170  aks4d1p8  42179  posbezout  42192  primrootspoweq0  42198  aks6d1c1  42208  hashscontpow1  42213  aks6d1c4  42216  aks6d1c2  42222  aks6d1c5lem1  42228  aks6d1c5lem3  42229  aks6d1c5lem2  42230  deg1gprod  42232  sticksstones7  42244  sticksstones10  42247  sticksstones12  42250  sticksstones22  42260  aks6d1c6lem1  42262  aks6d1c6lem3  42264  aks6d1c6lem4  42265  bcled  42270  bcle2d  42271  aks6d1c7lem1  42272  unitscyglem4  42290  aks5lem7  42292  aks5  42296  explt1d  42415  mulgt0b2d  42570  evlselv  42679  dffltz  42726  fltdvdsabdvdsc  42730  fltaccoprm  42732  fltabcoprm  42734  flt4lem5elem  42743  flt4lem7  42751  fltnlta  42755  irrapxlem1  42914  pell1qrgaplem  42965  pell1qrgap  42966  monotoddzzfi  43034  jm2.24nn  43051  congtr  43057  congmul  43059  congsub  43062  fzmaxdif  43073  acongeq  43075  jm2.20nn  43089  jm2.25  43091  hbtlem4  43218  dgrsub2  43227  mpaaeu  43242  idomsubgmo  43285  iscard4  43625  sqrtcvallem4  43731  leeq2d  44250  int-sqgeq0d  44278  int-ineqmvtd  44283  cvgdvgrat  44405  radcnvrat  44406  hashnzfzclim  44414  dvconstbi  44426  binomcxplemdvbinom  44445  isosctrlem1ALT  45025  mulltgt0  45118  rnmptbd2lem  45344  oddfl  45378  2timesgt  45388  lt3addmuld  45401  lt4addmuld  45406  supxrgere  45431  supxrgelem  45435  supxrge  45436  xadd0ge2  45439  infrpge  45449  xrlexaddrp  45450  xralrple2  45452  infxr  45464  infleinflem1  45467  infleinflem2  45468  infleinf  45469  xralrple4  45470  xralrple3  45471  recnnltrp  45474  rpgtrecnn  45477  xrralrecnnge  45487  rexabslelem  45515  infrnmptle  45520  supminfxr  45561  xrpnf  45582  iccshift  45617  iooshift  45621  ressiocsup  45653  ressioosup  45654  fsumnncl  45671  fmul01  45679  fmul01lt1lem1  45683  fmul01lt1lem2  45684  mccllem  45696  climrec  45702  climexp  45704  climneg  45709  limcrecl  45728  sumnnodd  45729  lptioo2  45730  lptioo1  45731  ltmod  45735  lptre2pt  45737  0ellimcdiv  45746  limclner  45748  fnlimcnv  45764  climinf2lem  45803  limsupubuzlem  45809  limsup10exlem  45869  limsupgtlem  45874  dfxlim2v  45944  xlimliminflimsup  45959  cncficcgt0  45985  cncfioobdlem  45993  ioodvbdlimc1lem1  46028  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  dvdsn1add  46036  dvnxpaek  46039  dvnmul  46040  dvnprodlem1  46043  itgiccshift  46077  itgperiod  46078  sublevolico  46081  ismbl3  46083  ovolsplit  46085  ismbl4  46090  stoweidlem1  46098  stoweidlem11  46108  stoweidlem13  46110  stoweidlem26  46123  stoweidlem34  46131  stoweidlem38  46135  stoweidlem42  46139  stoweidlem51  46148  stoweidlem59  46156  stirlinglem5  46175  stirlinglem6  46176  stirlinglem7  46177  stirlinglem10  46180  stirlinglem11  46181  stirlinglem13  46183  stirlinglem15  46185  dirkercncflem1  46200  dirkercncflem4  46203  fourierdlem4  46208  fourierdlem10  46214  fourierdlem11  46215  fourierdlem15  46219  fourierdlem20  46224  fourierdlem25  46229  fourierdlem26  46230  fourierdlem30  46234  fourierdlem37  46241  fourierdlem39  46243  fourierdlem40  46244  fourierdlem41  46245  fourierdlem42  46246  fourierdlem44  46248  fourierdlem47  46250  fourierdlem48  46251  fourierdlem49  46252  fourierdlem50  46253  fourierdlem51  46254  fourierdlem52  46255  fourierdlem54  46257  fourierdlem60  46263  fourierdlem61  46264  fourierdlem63  46266  fourierdlem64  46267  fourierdlem65  46268  fourierdlem73  46276  fourierdlem74  46277  fourierdlem75  46278  fourierdlem76  46279  fourierdlem78  46281  fourierdlem79  46282  fourierdlem81  46284  fourierdlem84  46287  fourierdlem87  46290  fourierdlem92  46295  fourierdlem93  46296  fourierdlem101  46304  fourierdlem102  46305  fourierdlem103  46306  fourierdlem104  46307  fourierdlem111  46314  fourierdlem114  46317  sqwvfoura  46325  sqwvfourb  46326  fouriersw  46328  etransclem19  46350  etransclem23  46354  etransclem24  46355  etransclem25  46356  etransclem27  46358  etransclem32  46363  etransclem35  46366  etransclem48  46379  qndenserrnbllem  46391  ioorrnopnlem  46401  ioorrnopnxrlem  46403  fsumlesge0  46474  sge0cl  46478  sge0supre  46486  sge0less  46489  sge0gerp  46492  sge0ltfirp  46497  sge0le  46504  sge0ltfirpmpt  46505  sge0split  46506  sge0rpcpnf  46518  sge0ltfirpmpt2  46523  sge0isum  46524  sge0xaddlem1  46530  sge0pnffigtmpt  46537  sge0pnffsumgt  46539  sge0gtfsumgt  46540  sge0seq  46543  nnfoctbdjlem  46552  meassle  46560  meaiuninclem  46577  meaiininclem  46583  omeiunle  46614  omeiunltfirp  46616  carageniuncllem2  46619  carageniuncl  46620  omess0  46631  hoicvr  46645  ovnlerp  46659  ovnsubaddlem1  46667  hsphoidmvle2  46682  hoidmv1lelem2  46689  hoidmv1le  46691  hoidmvlelem1  46692  hoidmvlelem2  46693  hoidmvlelem3  46694  hoidmvlelem5  46696  ovnhoilem2  46699  ovnhoi  46700  hoidifhspdmvle  46717  hoiqssbllem2  46720  hspmbllem2  46724  hspmbllem3  46725  hspmbl  46726  vonioolem2  46778  vonicclem2  46781  smfaddlem1  46860  smflimlem2  46869  smflimlem4  46871  smfmullem1  46888  smfinflem  46914  smflimsuplem4  46920  smflimsuplem8  46924  chnsubseq  46977  perfectALTVlem2  47821  nnpw2blen  48680  itscnhlinecirc02plem1  48882  funcoppc3  49247  oppcuprcl2  49302  isinito3  49600