Theorem breqtrd 5131

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breqtrrd  5133  breqtrid  5142  domunsn  9125  mapdom2  9146  phplem2  9199  mapfien2  9379  wemaplem2  9519  infdifsn  9636  cantnff  9653  ttrclss  9699  rnttrcl  9701  infxpenlem  10049  infmap2  10252  ssfin4  10345  canthp1lem1  10694  nqereq  10977  ltexnq  11017  ltbtwnnq  11020  add20  11783  mullt0  11790  ltm1  12114  recgt0  12118  prodgt0  12119  ltmul1a  12121  mulge0b  12142  recp1lt1  12170  recreclt  12171  ledivp1  12174  ledivp1i  12197  ltdivp1i  12198  eluzmn  12927  ltaddrp2d  13153  mul2lt0bi  13183  prodge0rd  13184  xleadd1a  13338  xov1plusxeqvd  13584  fz01en  13640  fzonmapblen  13797  fladdz  13919  flhalf  13924  fldiv  13954  modsubdir  14037  fzen2  14066  serle  14154  ltexp2a  14263  leexp2a  14269  exple1  14274  expubnd  14275  bernneq  14326  expmulnbnd  14332  discr1  14336  discr  14337  faclbnd6  14396  hashfz  14525  hashfun  14535  seqcoll  14562  sqeqd  15286  01sqrexlem7  15368  sqrtge0  15377  sqrtneglem  15386  abslt  15435  absle  15436  abstri  15451  rlimge0  15701  reccn2  15717  climaddc2  15756  isercolllem1  15785  caucvgrlem  15793  summolem2a  15834  isumge0  15885  fsumle  15919  fsumlt  15920  o1fsum  15933  supcvg  15978  expcnv  15986  geolim  15992  geolim2  15993  georeclim  15994  geo2lim  15997  mertenslem1  16006  mertens  16008  prodmolem2a  16054  efcllem  16196  ef0lem  16197  efgt0  16224  eftlub  16230  eflt  16238  sinbnd  16301  cosbnd  16302  ef01bndlem  16305  sin01gt0  16311  cos01gt0  16312  sin02gt0  16313  eirrlem  16325  rpnnen2lem11  16345  rpnnen2lem12  16346  ruclem11  16361  dvdssub2  16424  dvdsadd2b  16429  dvdsexp  16451  3dvds  16454  opoe  16486  bitsfzolem  16557  bitsinv1lem  16564  bezoutlem4  16665  dvdsgcd  16667  dvdsmulgcd  16679  bezoutr1  16692  nn0seqcvgd  16693  rpmulgcd2  16779  qredeq  16780  rpdvds  16783  prmind2  16808  divdenle  16873  hashdvds  16899  phimullem  16903  eulerthlem2  16906  prmdiveq  16910  prmdivdiv  16911  pythagtriplem4  16944  pythagtriplem10  16945  pythagtriplem19  16958  iserodd  16960  pcpre1  16967  pcadd2  17015  qexpz  17026  expnprm  17027  oddprmdvds  17028  pockthlem  17030  prmreclem2  17042  prmreclem3  17043  4sqlem7  17069  4sqlem10  17072  4sqlem11  17080  4sqlem12  17081  4sqlem14  17083  4sqlem15  17084  4sqlem16  17085  0ram  17145  ffthiso  18053  latmlej12  18600  qusgrp  19348  pgpfi1  19756  sylow1lem4  19762  sylow1lem5  19763  odcau  19765  pgpfi  19766  pgpssslw  19775  sylow3lem4  19791  sylow3lem6  19793  efgsfo  19900  frgp0  19921  odadd1  20009  odadd2  20010  odadd  20011  gexexlem  20013  lt6abl  20056  gsumzsubmcl  20079  pwsgsum  20143  dprd2dlem1  20204  dprd2d2  20207  ablfacrplem  20228  ablfacrp  20229  ablfacrp2  20230  ablfac1b  20233  ablfac1eu  20236  pgpfac1lem3a  20239  ablfaclem2  20249  dvdsrid  20544  dvdsrtr  20545  dvdsrneg  20547  unitmulcl  20557  unitgrp  20560  unitnegcl  20574  subrguss  20786  subrgunit  20789  isdrng2  20944  fidomndrnglem  20977  abvsubtri  21031  orngsqr  21070  ornglmulle  21071  orngrmulle  21072  orng0le1  21078  gzrngunit  21686  prmirredlem  21725  znidomb  21814  frlmgsum  22025  psrbaglesupp  22177  psdmul  22434  psdmvr  22437  invrvald  22938  psmetsym  24576  psmettri  24577  mettri2  24607  xmetsym  24613  xmettri  24617  prdsxmetlem  24634  xblss2ps  24667  xblss2  24668  blhalf  24671  xmsge0  24729  ngptgp  24902  nrginvrcnlem  24957  nmoeq0  25002  cnmet  25037  blcvx  25064  opnreen  25098  metdcnlem  25103  metdstri  25118  metdsle  25119  metnrmlem1  25126  metnrmlem3  25128  lebnumlem1  25229  pi1inv  25320  cphnmf  25463  ipge0  25466  ipcau2  25502  tcphcphlem1  25503  csbren  25667  minveclem2  25694  minveclem3  25697  ovolssnul  25755  ovolctb  25758  ovolunnul  25768  ovoliunlem1  25770  ovoliun2  25774  ovoliunnul  25775  ioombl1lem4  25829  uniioombllem3  25853  uniioombllem4  25854  uniioombllem5  25855  uniioombl  25857  volcn  25874  vitalilem2  25877  vitalilem5  25880  itg1lea  25980  mbfi1fseqlem6  25988  mbfi1flimlem  25990  itg2eqa  26013  itg2splitlem  26016  itg2split  26017  itg2monolem1  26018  itg2cnlem2  26030  iblabsr  26097  iblmulc2  26098  bddiblnc  26109  dveflem  26246  dvef  26247  dvferm2lem  26253  dvlip  26260  c1liplem1  26263  dveq0  26267  dvlt0  26272  dvivthlem1  26275  lhop1  26281  dvfsumle  26288  dvfsumlem4  26296  dvfsumrlim3  26300  dvfsum2  26301  ftc1a  26304  ftc1lem4  26306  deg1add  26368  ply1divex  26402  ply1rem  26431  fta1glem2  26434  fta1blem  26436  ig1pdvds  26445  plyeq0lem  26476  dgrcolem2  26540  plydivlem4  26566  plyrem  26575  fta1lem  26577  aalioulem3  26610  aaliou2b  26617  aaliou3lem3  26620  aaliou3lem8  26621  ulmcn  26675  ulmdvlem1  26676  itgulm  26684  pserulm  26698  pserdvlem2  26704  abelthlem2  26708  abelthlem5  26711  abelthlem6  26712  abelthlem7  26714  abelthlem8  26715  abelthlem9  26716  sinq12gt0  26785  sinq34lt0t  26787  cosq14gt0  26788  cosq14ge0  26789  cos02pilt1  26803  efif1olem3  26821  argimgt0  26889  argimlt0  26890  logneg2  26892  logcnlem3  26921  logcnlem4  26922  logtayllem  26936  logtayl2  26939  cxpsqrtlem  26979  cxpsqrt  26980  cxpaddlelem  27028  abscxpbnd  27030  zrtdvds  27036  rtprmirr  27037  loglesqrt  27038  ang180lem2  27087  atanlogaddlem  27190  atanlogsublem  27192  atantan  27200  atans2  27208  atantayl  27214  leibpi  27219  log2tlbnd  27222  birthdaylem2  27229  birthdaylem3  27230  cxp2limlem  27252  jensenlem2  27264  jensen  27265  logdiflbnd  27271  emcllem2  27273  emcllem4  27275  harmonicbnd4  27287  fsumharmonic  27288  lgamgulmlem2  27306  lgamgulm2  27312  lgambdd  27313  lgamucov  27314  lgamcvglem  27316  lgamcvg2  27331  gamcvg  27332  wilthlem3  27346  basellem1  27357  basellem3  27359  basellem4  27360  fsumdvdsdiaglem  27459  dvdsppwf1o  27462  mpodvdsmulf1o  27470  dvdsmulf1o  27472  chteq0  27485  chtub  27488  chpub  27496  logfacubnd  27497  logfaclbnd  27498  logexprlim  27501  perfectlem2  27506  dchrfi  27531  bclbnd  27556  bposlem1  27560  bposlem3  27562  bposlem4  27563  bposlem6  27565  lgslem1  27573  lgsqrlem2  27623  lgsqrlem4  27625  lgseisenlem2  27652  lgsquadlem1  27656  lgsquadlem2  27657  lgsquad2lem1  27660  2sqlem3  27696  2sqlem4  27697  2sqlem8  27702  2sqlem11  27705  2sqcoprm  27711  2sqmod  27712  chebbnd1lem2  27746  chebbnd1lem3  27747  chtppilimlem1  27749  chpchtlim  27755  vmadivsum  27758  vmadivsumb  27759  rpvmasumlem  27763  dchrisumlem2  27766  dchrmusum2  27770  dchrvmasumlem2  27774  dchrvmasumlem3  27775  dchrisum0flblem2  27785  dchrisum0fno1  27787  dchrisum0re  27789  dchrisum0lem1  27792  dchrisum0lem2a  27793  mudivsum  27806  mulogsumlem  27807  mulog2sumlem2  27811  vmalogdivsum2  27814  selberglem2  27822  selbergb  27825  selberg2b  27828  logdivbnd  27832  selberg3lem1  27833  selberg3lem2  27834  selberg4lem1  27836  pntrmax  27840  pntrlog2bndlem2  27854  pntrlog2bndlem3  27855  pntrlog2bndlem5  27857  pntrlog2bndlem6a  27858  pntrlog2bndlem6  27859  pntrlog2bnd  27860  pntpbnd1a  27861  pntpbnd1  27862  pntpbnd2  27863  pntibndlem1  27865  pntibndlem2  27867  pntlemb  27873  pntlemq  27877  pntlemr  27878  pntlemj  27879  pntlemk  27882  qabvle  27901  padicabvcxp  27908  ostth2lem2  27910  ostth2lem3  27911  ostth2lem4  27912  ostth3  27914  addsuniflem  28306  negsid  28346  negsunif  28360  negright  28364  mulsuniflem  28454  ltmuls2  28476  precsexlem9  28520  absmuls  28549  zcuts  28712  addhalfcut  28764  pw2cut2  28767  bdayfinbndlem1  28772  z12sge0  28788  legtrid  28973  legov3  28980  krippenlem  29081  mideulem2  29129  midex  29132  opphllem5  29146  opphllem6  29147  opphl  29149  lmieu  29208  lmiisolem  29220  perpeqlem  29266  angmgmaddcpbl  29309  prlnghpg  29343  perpprlng  29347  prlngsymquadlem  29360  quadcgrprlng  29363  tgaltai  29364  ttgcontlem1  29381  colinearalglem4  29406  axpaschlem  29437  axcontlem7  29467  nbfusgrlevtxm2  29878  clwlksndivn  30596  eucrct2eupth  30765  nvge0  31194  smcnlem  31218  nmoub3i  31294  nmoub2i  31295  nmlno0lem  31314  minvecolem2  31396  htthlem  31438  norm3dif2  31672  bcs2  31703  chscllem2  32159  eigposi  32357  nmopub2tALT  32430  nmfnleub2  32447  nmlnop0iALT  32516  riesz1  32586  cnlnadjlem2  32589  nmopcoadji  32622  leopsq  32650  leopmul  32655  leopnmid  32659  nmopleid  32660  opsqrlem6  32666  0leopj  32707  hstle1  32747  strlem3a  32773  mdslmd4i  32854  cvexchlem  32889  cdj1i  32954  unidifsnel  33050  unidifsnne  33051  le2halvesd  33267  xlt2addrd  33270  fsumub  33338  sgnmulsgp  33342  2exple2exp  33344  oexpled  33346  wrdt2ind  33435  xrge0tsmsd  33553  fzto1st1  33582  cycpmco2lem4  33609  cycpmco2lem6  33611  cyc3conja  33637  archiabllem1a  33671  archiabllem2a  33674  archiabllem2c  33675  rprmdvdsprod  33985  1arithidomlem1  33986  1arithidomlem2  33987  1arithidom  33988  ply1dg3rt0irred  34035  mplmulmvr  34090  mplvrpmrhm  34098  exsslsb  34148  fedgmullem1  34180  fedgmullem2  34181  fldsdrgfldext2  34213  fldextrspundgdvdslem  34231  fldextrspundgdvds  34232  fldext2rspun  34233  extdgfialglem2  34244  algextdeglem8  34275  rtelextdg2lem  34277  constrext2chnlem  34301  cos9thpiminplylem1  34333  cos9thpiminplylem2  34334  metideq  34444  metider  34445  sqsscirc1  34459  esummono  34605  esumpad2  34607  esumle  34609  esumlef  34613  esumcst  34614  esumrnmpt2  34619  esum2d  34644  aean  34796  dya2ub  34822  dya2icoseg  34829  omssubadd  34852  inelcarsg  34863  carsgsigalem  34867  carsggect  34870  carsgclctunlem2  34871  eulerpartlemb  34920  fibp1  34953  signsplypnf  35099  signsply0  35100  fdvposlt  35148  fdvposle  35150  reprgt  35170  logdivsqrle  35199  hgt750lemb  35205  hgt750leme  35207  tgoldbachgtde  35209  subfacval3  35869  sconnpht2  35918  sconnpi1  35919  resconn  35926  snmlff  36009  sinccvglem  36352  faclimlem2  36424  btwnouttr2  36703  weiunpo  37169  dnibndlem5  37264  dnibndlem7  37266  dnibndlem8  37267  dnibndlem9  37268  dnibndlem10  37269  dnibnd  37273  knoppcnlem4  37278  knoppcnlem9  37283  unbdqndv2lem1  37291  unbdqndv2lem2  37292  knoppndvlem11  37304  knoppndvlem12  37305  knoppndvlem14  37307  knoppndvlem15  37308  knoppndvlem17  37310  knoppndvlem18  37311  knoppndvlem19  37312  knoppndvlem21  37314  ltflcei  38445  poimirlem9  38461  poimirlem26  38478  poimirlem27  38479  poimirlem29  38481  heicant  38487  mblfinlem2  38490  mblfinlem3  38491  mblfinlem4  38492  volsupnfl  38497  itg2addnclem  38503  itg2addnclem3  38505  iblmulc2nc  38517  ftc1cnnclem  38523  ftc1anclem6  38530  ftc1anclem7  38531  ftc1anclem8  38532  ftc2nc  38534  dvasin  38536  geomcau  38607  bfplem2  38671  rrncmslem  38680  rrnequiv  38683  lsatcvatlem  40020  islshpcv  40024  atlatmstc  40290  cvlsupr7  40319  cvrval3  40384  cvrval5  40386  cvrexchlem  40390  atcvrj1  40402  cvrat3  40413  cvrat4  40414  atbtwn  40417  1cvratex  40444  hlatexch4  40452  3atlem1  40454  3atlem2  40455  atcvrlln2  40490  atcvrlln  40491  lplnllnneN  40527  llncvrlpln2  40528  4atlem3b  40569  lplncvrlvol2  40586  dalemswapyz  40627  dalemswapyzps  40661  dalem25  40669  dalem39  40682  dalem58  40701  dalem59  40702  lneq2at  40749  lncvrat  40753  dalawlem2  40843  dalawlem3  40844  dalawlem4  40845  dalawlem6  40847  dalawlem9  40850  dalawlem11  40852  dalawlem12  40853  lhpocnle  40987  lhpmcvr3  40996  lhpmcvr5N  40998  lhpmcvr6N  40999  4atexlemunv  41037  4atexlemc  41040  4atexlemex2  41042  lautm  41065  cdlemc2  41163  cdleme5  41211  cdleme11j  41238  cdleme16b  41250  cdlemednpq  41270  cdleme19e  41278  cdleme20i  41288  cdleme22a  41311  cdleme22cN  41313  cdleme22d  41314  cdleme22e  41315  cdleme22eALTN  41316  cdleme22f  41317  cdleme23c  41322  cdleme30a  41349  cdleme35a  41419  cdleme35b  41421  cdleme42h  41453  cdlemeg46rgv  41499  cdlemg8b  41599  cdlemg12e  41618  cdlemg13a  41622  cdlemg17pq  41643  cdlemg18c  41651  cdlemg19  41655  cdlemg21  41657  cdlemg31d  41671  cdlemg33a  41677  tendoid  41744  cdlemk4  41805  cdlemki  41812  cdlemk10  41814  cdlemksv2  41818  cdlemk12  41821  cdlemk14  41825  cdlemk15  41826  cdlemk1u  41830  cdlemk5u  41832  cdlemk12u  41843  cdlemk45  41918  cdlemk48  41921  dia2dimlem1  42035  dia2dimlem2  42036  dia2dimlem3  42037  cdlemm10N  42089  cdlemn2  42166  dihjustlem  42187  dihglbcpreN  42271  dihmeetlem3N  42276  nnproddivdvdsd  42964  lcmineqlem17  43009  lcmineqlem18  43010  3lexlogpow2ineq1  43022  3lexlogpow2ineq2  43023  3lexlogpow5ineq5  43024  aks4d1p1p3  43033  aks4d1p1p2  43034  aks4d1p1p4  43035  aks4d1p1p5  43039  aks4d1p1  43040  aks4d1p3  43042  aks4d1p8  43051  posbezout  43064  primrootspoweq0  43070  aks6d1c1  43080  hashscontpow1  43085  aks6d1c4  43088  aks6d1c2  43094  aks6d1c5lem1  43100  aks6d1c5lem3  43101  aks6d1c5lem2  43102  deg1gprod  43104  sticksstones7  43116  sticksstones10  43119  sticksstones12  43122  sticksstones22  43132  aks6d1c6lem1  43134  aks6d1c6lem3  43136  aks6d1c6lem4  43137  bcled  43142  bcle2d  43143  aks6d1c7lem1  43144  unitscyglem4  43162  aks5lem7  43164  aks5  43168  explt1d  43296  mulgt0b2d  43464  evlselv  43533  dffltz  43578  fltdvdsabdvdsc  43582  fltaccoprm  43584  fltabcoprm  43586  flt4lem5elem  43595  flt4lem7  43603  fltnlta  43607  irrapxlem1  43761  pell1qrgaplem  43812  pell1qrgap  43813  monotoddzzfi  43881  jm2.24nn  43898  congtr  43904  congmul  43906  congsub  43909  fzmaxdif  43920  acongeq  43922  jm2.20nn  43936  jm2.25  43938  hbtlem4  44065  dgrsub2  44074  mpaaeu  44089  idomsubgmo  44132  iscard4  44471  sqrtcvallem4  44577  leeq2d  45096  int-sqgeq0d  45124  int-ineqmvtd  45129  cvgdvgrat  45235  radcnvrat  45236  hashnzfzclim  45244  dvconstbi  45256  binomcxplemdvbinom  45275  isosctrlem1ALT  45854  mulltgt0  45954  rnmptbd2lem  46175  oddfl  46209  2timesgt  46219  lt3addmuld  46232  lt4addmuld  46237  supxrgere  46261  supxrgelem  46265  supxrge  46266  xadd0ge2  46269  infrpge  46279  xrlexaddrp  46280  xralrple2  46282  infxr  46294  infleinflem1  46297  infleinflem2  46298  infleinf  46299  xralrple4  46300  xralrple3  46301  recnnltrp  46304  rpgtrecnn  46307  xrralrecnnge  46317  rexabslelem  46344  infrnmptle  46349  supminfxr  46390  xrpnf  46411  iccshift  46446  iooshift  46450  ressiocsup  46482  ressioosup  46483  fsumnncl  46500  fmul01  46508  fmul01lt1lem1  46512  fmul01lt1lem2  46513  mccllem  46525  climrec  46531  climexp  46533  climneg  46538  limcrecl  46557  sumnnodd  46558  lptioo2  46559  lptioo1  46560  ltmod  46564  lptre2pt  46566  0ellimcdiv  46575  limclner  46577  fnlimcnv  46593  climinf2lem  46632  limsupubuzlem  46638  limsup10exlem  46698  limsupgtlem  46703  dfxlim2v  46773  xlimliminflimsup  46788  cncficcgt0  46814  cncfioobdlem  46822  ioodvbdlimc1lem1  46857  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  dvdsn1add  46865  dvnxpaek  46868  dvnmul  46869  dvnprodlem1  46872  itgiccshift  46906  itgperiod  46907  sublevolico  46910  ismbl3  46912  ovolsplit  46914  ismbl4  46919  stoweidlem1  46927  stoweidlem11  46937  stoweidlem13  46939  stoweidlem26  46952  stoweidlem34  46960  stoweidlem38  46964  stoweidlem42  46968  stoweidlem51  46977  stoweidlem59  46985  stirlinglem5  47004  stirlinglem6  47005  stirlinglem7  47006  stirlinglem10  47009  stirlinglem11  47010  stirlinglem13  47012  stirlinglem15  47014  dirkercncflem1  47029  dirkercncflem4  47032  fourierdlem4  47037  fourierdlem10  47043  fourierdlem11  47044  fourierdlem15  47048  fourierdlem20  47053  fourierdlem25  47058  fourierdlem26  47059  fourierdlem30  47063  fourierdlem37  47070  fourierdlem39  47072  fourierdlem40  47073  fourierdlem41  47074  fourierdlem42  47075  fourierdlem44  47077  fourierdlem47  47079  fourierdlem48  47080  fourierdlem49  47081  fourierdlem50  47082  fourierdlem51  47083  fourierdlem52  47084  fourierdlem54  47086  fourierdlem60  47092  fourierdlem61  47093  fourierdlem63  47095  fourierdlem64  47096  fourierdlem65  47097  fourierdlem73  47105  fourierdlem74  47106  fourierdlem75  47107  fourierdlem76  47108  fourierdlem78  47110  fourierdlem79  47111  fourierdlem81  47113  fourierdlem84  47116  fourierdlem87  47119  fourierdlem92  47124  fourierdlem93  47125  fourierdlem101  47133  fourierdlem102  47134  fourierdlem103  47135  fourierdlem104  47136  fourierdlem111  47143  fourierdlem114  47146  sqwvfoura  47154  sqwvfourb  47155  fouriersw  47157  etransclem19  47179  etransclem23  47183  etransclem24  47184  etransclem25  47185  etransclem27  47187  etransclem32  47192  etransclem35  47195  etransclem48  47208  qndenserrnbllem  47220  ioorrnopnlem  47230  ioorrnopnxrlem  47232  fsumlesge0  47303  sge0cl  47307  sge0supre  47315  sge0less  47318  sge0gerp  47321  sge0ltfirp  47326  sge0le  47333  sge0ltfirpmpt  47334  sge0split  47335  sge0rpcpnf  47347  sge0ltfirpmpt2  47352  sge0isum  47353  sge0xaddlem1  47359  sge0pnffigtmpt  47366  sge0pnffsumgt  47368  sge0gtfsumgt  47369  sge0seq  47372  nnfoctbdjlem  47381  meassle  47389  meaiuninclem  47406  meaiininclem  47412  omeiunle  47443  omeiunltfirp  47445  carageniuncllem2  47448  carageniuncl  47449  omess0  47460  hoicvr  47474  ovnlerp  47488  ovnsubaddlem1  47496  hsphoidmvle2  47511  hoidmv1lelem2  47518  hoidmv1le  47520  hoidmvlelem1  47521  hoidmvlelem2  47522  hoidmvlelem3  47523  hoidmvlelem5  47525  ovnhoilem2  47528  ovnhoi  47529  hoidifhspdmvle  47546  hoiqssbllem2  47549  hspmbllem2  47553  hspmbllem3  47554  hspmbl  47555  vonioolem2  47607  vonicclem2  47610  smfaddlem1  47689  smflimlem2  47698  smflimlem4  47700  smfmullem1  47717  smfinflem  47743  smflimsuplem4  47749  smflimsuplem8  47753  chnsubseq  47806  sqrtnpoly  47859  perfectALTVlem2  48736  nnpw2blen  49608  itscnhlinecirc02plem1  49810  funcoppc3  50171  oppcuprcl2  50226  isinito3  50524