Theorem breqtrd 5134

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  breqtrrd  5136  breqtrid  5145  domunsn  9171  mapdom2  9192  phplem2  9245  mapfien2  9425  wemaplem2  9565  infdifsn  9682  cantnff  9699  ttrclss  9745  rnttrcl  9747  infxpenlem  10116  infmap2  10319  ssfin4  10412  canthp1lem1  10761  nqereq  11044  ltexnq  11084  ltbtwnnq  11087  add20  11852  mullt0  11859  ltm1  12183  recgt0  12187  prodgt0  12188  ltmul1a  12190  mulge0b  12211  recp1lt1  12239  recreclt  12240  ledivp1  12243  ledivp1i  12266  ltdivp1i  12267  eluzmn  12996  ltaddrp2d  13222  mul2lt0bi  13252  prodge0rd  13253  xleadd1a  13407  xov1plusxeqvd  13653  fz01en  13710  fzonmapblen  13867  fladdz  13989  flhalf  13994  fldiv  14024  modsubdir  14107  fzen2  14136  serle  14224  ltexp2a  14333  leexp2a  14339  exple1  14344  expubnd  14345  bernneq  14397  expmulnbnd  14403  discr1  14407  discr  14408  faclbnd6  14467  hashfz  14596  hashfun  14606  seqcoll  14633  sqeqd  15359  01sqrexlem7  15441  sqrtge0  15450  sqrtneglem  15459  abslt  15508  absle  15509  abstri  15524  rlimge0  15774  reccn2  15790  climaddc2  15829  isercolllem1  15858  caucvgrlem  15866  summolem2a  15907  isumge0  15958  fsumle  15992  fsumlt  15993  o1fsum  16006  supcvg  16051  expcnv  16059  geolim  16065  geolim2  16066  georeclim  16067  geo2lim  16070  mertenslem1  16079  mertens  16081  prodmolem2a  16127  efcllem  16269  ef0lem  16270  efgt0  16297  eftlub  16303  eflt  16311  sinbnd  16374  cosbnd  16375  ef01bndlem  16378  sin01gt0  16384  cos01gt0  16385  sin02gt0  16386  eirrlem  16398  rpnnen2lem11  16418  rpnnen2lem12  16419  ruclem11  16434  dvdssub2  16497  dvdsadd2b  16502  dvdsexp  16524  3dvds  16527  opoe  16559  bitsfzolem  16630  bitsinv1lem  16637  bezoutlem4  16741  dvdsgcd  16743  dvdsmulgcd  16756  bezoutr1  16770  nn0seqcvgd  16771  rpmulgcd2  16857  qredeq  16858  rpdvds  16861  prmind2  16886  divdenle  16951  hashdvds  16978  phimullem  16982  eulerthlem2  16985  prmdiveq  16989  prmdivdiv  16990  pythagtriplem4  17023  pythagtriplem10  17024  pythagtriplem19  17037  iserodd  17039  pcpre1  17046  pcadd2  17094  qexpz  17105  expnprm  17106  oddprmdvds  17107  pockthlem  17109  prmreclem2  17121  prmreclem3  17122  4sqlem7  17148  4sqlem10  17151  4sqlem11  17159  4sqlem12  17160  4sqlem14  17162  4sqlem15  17163  4sqlem16  17164  0ram  17224  ffthiso  18132  latmlej12  18679  qusgrp  19427  pgpfi1  19836  sylow1lem4  19842  sylow1lem5  19843  odcau  19845  pgpfi  19846  pgpssslw  19855  sylow3lem4  19871  sylow3lem6  19873  efgsfo  19980  frgp0  20001  odadd1  20089  odadd2  20090  odadd  20091  gexexlem  20093  lt6abl  20136  gsumzsubmcl  20159  pwsgsum  20223  dprd2dlem1  20284  dprd2d2  20287  ablfacrplem  20308  ablfacrp  20309  ablfacrp2  20310  ablfac1b  20313  ablfac1eu  20316  pgpfac1lem3a  20319  ablfaclem2  20329  dvdsrid  20624  dvdsrtr  20625  dvdsrneg  20627  unitmulcl  20637  unitgrp  20640  unitnegcl  20654  subrguss  20866  subrgunit  20869  isdrng2  21024  fidomndrnglem  21057  abvsubtri  21111  orngsqr  21150  ornglmulle  21151  orngrmulle  21152  orng0le1  21158  gzrngunit  21766  prmirredlem  21805  znidomb  21894  frlmgsum  22105  psrbaglesupp  22257  psdmul  22514  psdmvr  22517  invrvald  23018  psmetsym  24656  psmettri  24657  mettri2  24687  xmetsym  24693  xmettri  24697  prdsxmetlem  24714  xblss2ps  24747  xblss2  24748  blhalf  24751  xmsge0  24809  ngptgp  24982  nrginvrcnlem  25037  nmoeq0  25082  cnmet  25117  blcvx  25144  opnreen  25178  metdcnlem  25183  metdstri  25198  metdsle  25199  metnrmlem1  25206  metnrmlem3  25208  lebnumlem1  25309  pi1inv  25400  cphnmf  25543  ipge0  25546  ipcau2  25582  tcphcphlem1  25583  csbren  25747  minveclem2  25774  minveclem3  25777  ovolssnul  25835  ovolctb  25838  ovolunnul  25848  ovoliunlem1  25850  ovoliun2  25854  ovoliunnul  25855  ioombl1lem4  25909  uniioombllem3  25933  uniioombllem4  25934  uniioombllem5  25935  uniioombl  25937  volcn  25954  vitalilem2  25957  vitalilem5  25960  itg1lea  26060  mbfi1fseqlem6  26068  mbfi1flimlem  26070  itg2eqa  26093  itg2splitlem  26096  itg2split  26097  itg2monolem1  26098  itg2cnlem2  26110  iblabsr  26177  iblmulc2  26178  bddiblnc  26189  dveflem  26326  dvef  26327  dvferm2lem  26333  dvlip  26340  c1liplem1  26343  dveq0  26347  dvlt0  26352  dvivthlem1  26355  lhop1  26361  dvfsumle  26368  dvfsumlem4  26376  dvfsumrlim3  26380  dvfsum2  26381  ftc1a  26384  ftc1lem4  26386  deg1add  26448  ply1divex  26482  ply1rem  26511  fta1glem2  26514  fta1blem  26516  ig1pdvds  26525  plyeq0lem  26556  dgrcolem2  26620  plydivlem4  26644  plyrem  26653  fta1lem  26655  aalioulem3  26688  aaliou2b  26695  aaliou3lem3  26698  aaliou3lem8  26699  ulmcn  26753  ulmdvlem1  26754  itgulm  26762  pserulm  26776  pserdvlem2  26782  abelthlem2  26786  abelthlem5  26789  abelthlem6  26790  abelthlem7  26792  abelthlem8  26793  abelthlem9  26794  sinq12gt0  26863  sinq34lt0t  26865  cosq14gt0  26866  cosq14ge0  26867  cos02pilt1  26881  efif1olem3  26899  argimgt0  26967  argimlt0  26968  logneg2  26970  logcnlem3  26999  logcnlem4  27000  logtayllem  27014  logtayl2  27017  cxpsqrtlem  27057  cxpsqrt  27058  cxpaddlelem  27106  abscxpbnd  27108  zrtdvds  27114  rtprmirr  27115  loglesqrt  27116  ang180lem2  27165  atanlogaddlem  27268  atanlogsublem  27270  atantan  27278  atans2  27286  atantayl  27292  leibpi  27297  log2tlbnd  27300  birthdaylem2  27307  birthdaylem3  27308  cxp2limlem  27330  jensenlem2  27342  jensen  27343  logdiflbnd  27349  emcllem2  27351  emcllem4  27353  harmonicbnd4  27365  fsumharmonic  27366  lgamgulmlem2  27384  lgamgulm2  27390  lgambdd  27391  lgamucov  27392  lgamcvglem  27394  lgamcvg2  27409  gamcvg  27410  wilthlem3  27424  basellem1  27435  basellem3  27437  basellem4  27438  fsumdvdsdiaglem  27537  dvdsppwf1o  27540  mpodvdsmulf1o  27548  dvdsmulf1o  27550  chteq0  27563  chtub  27566  chpub  27574  logfacubnd  27575  logfaclbnd  27576  logexprlim  27579  perfectlem2  27584  dchrfi  27609  bclbnd  27634  bposlem1  27638  bposlem3  27640  bposlem4  27641  bposlem6  27643  lgslem1  27651  lgsqrlem2  27701  lgsqrlem4  27703  lgseisenlem2  27730  lgsquadlem1  27734  lgsquadlem2  27735  lgsquad2lem1  27738  2sqlem3  27774  2sqlem4  27775  2sqlem8  27780  2sqlem11  27783  2sqcoprm  27789  2sqmod  27790  chebbnd1lem2  27824  chebbnd1lem3  27825  chtppilimlem1  27827  chpchtlim  27833  vmadivsum  27836  vmadivsumb  27837  rpvmasumlem  27841  dchrisumlem2  27844  dchrmusum2  27848  dchrvmasumlem2  27852  dchrvmasumlem3  27853  dchrisum0flblem2  27863  dchrisum0fno1  27865  dchrisum0re  27867  dchrisum0lem1  27870  dchrisum0lem2a  27871  mudivsum  27884  mulogsumlem  27885  mulog2sumlem2  27889  vmalogdivsum2  27892  selberglem2  27900  selbergb  27903  selberg2b  27906  logdivbnd  27910  selberg3lem1  27911  selberg3lem2  27912  selberg4lem1  27914  pntrmax  27918  pntrlog2bndlem2  27932  pntrlog2bndlem3  27933  pntrlog2bndlem5  27935  pntrlog2bndlem6a  27936  pntrlog2bndlem6  27937  pntrlog2bnd  27938  pntpbnd1a  27939  pntpbnd1  27940  pntpbnd2  27941  pntibndlem1  27943  pntibndlem2  27945  pntlemb  27951  pntlemq  27955  pntlemr  27956  pntlemj  27957  pntlemk  27960  qabvle  27979  padicabvcxp  27986  ostth2lem2  27988  ostth2lem3  27989  ostth2lem4  27990  ostth3  27992  fltdvdsabdvdsc  27997  fltaccoprm  27999  fltabcoprm  28001  flt4lem5elem  28008  flt4lem7  28016  addsuniflem  28414  negsid  28454  negsunif  28468  negright  28472  mulsuniflem  28562  ltmuls2  28584  precsexlem9  28628  absmuls  28657  zcuts  28820  addhalfcut  28872  pw2cut2  28875  bdayfinbndlem1  28880  z12sge0  28896  legtrid  29081  legov3  29088  krippenlem  29189  mideulem2  29237  midex  29240  opphllem5  29254  opphllem6  29255  opphl  29257  lmieu  29316  lmiisolem  29328  perpeqlem  29374  angmgmaddcpbl  29417  prlnghpg  29451  perpprlng  29455  prlngsymquadlem  29468  quadcgrprlng  29471  tgaltai  29472  ttgcontlem1  29489  colinearalglem4  29514  axpaschlem  29545  axcontlem7  29575  nbfusgrlevtxm2  29986  clwlksndivn  30704  eucrct2eupth  30873  nvge0  31302  smcnlem  31326  nmoub3i  31402  nmoub2i  31403  nmlno0lem  31422  minvecolem2  31504  htthlem  31546  norm3dif2  31780  bcs2  31811  chscllem2  32267  eigposi  32465  nmopub2tALT  32538  nmfnleub2  32555  nmlnop0iALT  32624  riesz1  32694  cnlnadjlem2  32697  nmopcoadji  32730  leopsq  32758  leopmul  32763  leopnmid  32767  nmopleid  32768  opsqrlem6  32774  0leopj  32815  hstle1  32855  strlem3a  32881  mdslmd4i  32962  cvexchlem  32997  cdj1i  33062  unidifsnel  33200  unidifsnne  33201  le2halvesd  33415  xlt2addrd  33418  fsumub  33486  sgnmulsgp  33490  2exple2exp  33492  oexpled  33494  wrdt2ind  33583  xrge0tsmsd  33701  fzto1st1  33730  cycpmco2lem4  33757  cycpmco2lem6  33759  cyc3conja  33785  archiabllem1a  33819  archiabllem2a  33822  archiabllem2c  33823  rprmdvdsprod  34133  1arithidomlem1  34134  1arithidomlem2  34135  1arithidom  34136  ply1dg3rt0irred  34183  mplmulmvr  34238  mplvrpmrhm  34246  exsslsb  34296  fedgmullem1  34328  fedgmullem2  34329  fldsdrgfldext2  34361  fldextrspundgdvdslem  34379  fldextrspundgdvds  34380  fldext2rspun  34381  extdgfialglem2  34392  algextdeglem8  34423  rtelextdg2lem  34425  constrext2chnlem  34449  cos9thpiminplylem1  34481  cos9thpiminplylem2  34482  metideq  34592  metider  34593  sqsscirc1  34607  esummono  34753  esumpad2  34755  esumle  34757  esumlef  34761  esumcst  34762  esumrnmpt2  34767  esum2d  34792  aean  34944  dya2ub  34969  dya2icoseg  34976  omssubadd  34999  inelcarsg  35010  carsgsigalem  35014  carsggect  35017  carsgclctunlem2  35018  eulerpartlemb  35067  fibp1  35100  signsplypnf  35246  signsply0  35247  fdvposlt  35295  fdvposle  35297  reprgt  35317  logdivsqrle  35346  hgt750lemb  35352  hgt750leme  35354  tgoldbachgtde  35356  subfacval3  36120  sconnpht2  36169  sconnpi1  36170  resconn  36177  snmlff  36260  sinccvglem  36603  faclimlem2  36686  btwnouttr2  36964  weiunpo  37430  dnibndlem5  37525  dnibndlem7  37527  dnibndlem8  37528  dnibndlem9  37529  dnibndlem10  37530  dnibnd  37534  knoppcnlem4  37539  knoppcnlem9  37544  unbdqndv2lem1  37552  unbdqndv2lem2  37553  knoppndvlem11  37565  knoppndvlem12  37566  knoppndvlem14  37568  knoppndvlem15  37569  knoppndvlem17  37571  knoppndvlem18  37572  knoppndvlem19  37573  knoppndvlem21  37575  ltflcei  38722  poimirlem9  38738  poimirlem26  38755  poimirlem27  38756  poimirlem29  38758  heicant  38764  mblfinlem2  38767  mblfinlem3  38768  mblfinlem4  38769  volsupnfl  38774  itg2addnclem  38780  itg2addnclem3  38782  iblmulc2nc  38794  ftc1cnnclem  38800  ftc1anclem6  38807  ftc1anclem7  38808  ftc1anclem8  38809  ftc2nc  38811  dvasin  38813  geomcau  38884  bfplem2  38948  rrncmslem  38957  rrnequiv  38960  lsatcvatlem  40297  islshpcv  40301  atlatmstc  40567  cvlsupr7  40596  cvrval3  40661  cvrval5  40663  cvrexchlem  40667  atcvrj1  40679  cvrat3  40690  cvrat4  40691  atbtwn  40694  1cvratex  40721  hlatexch4  40729  3atlem1  40731  3atlem2  40732  atcvrlln2  40767  atcvrlln  40768  lplnllnneN  40804  llncvrlpln2  40805  4atlem3b  40846  lplncvrlvol2  40863  dalemswapyz  40904  dalemswapyzps  40938  dalem25  40946  dalem39  40959  dalem58  40978  dalem59  40979  lneq2at  41026  lncvrat  41030  dalawlem2  41120  dalawlem3  41121  dalawlem4  41122  dalawlem6  41124  dalawlem9  41127  dalawlem11  41129  dalawlem12  41130  lhpocnle  41264  lhpmcvr3  41273  lhpmcvr5N  41275  lhpmcvr6N  41276  4atexlemunv  41314  4atexlemc  41317  4atexlemex2  41319  lautm  41342  cdlemc2  41440  cdleme5  41488  cdleme11j  41515  cdleme16b  41527  cdlemednpq  41547  cdleme19e  41555  cdleme20i  41565  cdleme22a  41588  cdleme22cN  41590  cdleme22d  41591  cdleme22e  41592  cdleme22eALTN  41593  cdleme22f  41594  cdleme23c  41599  cdleme30a  41626  cdleme35a  41696  cdleme35b  41698  cdleme42h  41730  cdlemeg46rgv  41776  cdlemg8b  41876  cdlemg12e  41895  cdlemg13a  41899  cdlemg17pq  41920  cdlemg18c  41928  cdlemg19  41932  cdlemg21  41934  cdlemg31d  41948  cdlemg33a  41954  tendoid  42021  cdlemk4  42082  cdlemki  42089  cdlemk10  42091  cdlemksv2  42095  cdlemk12  42098  cdlemk14  42102  cdlemk15  42103  cdlemk1u  42107  cdlemk5u  42109  cdlemk12u  42120  cdlemk45  42195  cdlemk48  42198  dia2dimlem1  42312  dia2dimlem2  42313  dia2dimlem3  42314  cdlemm10N  42366  cdlemn2  42443  dihjustlem  42464  dihglbcpreN  42548  dihmeetlem3N  42553  nnproddivdvdsd  43241  lcmineqlem17  43286  lcmineqlem18  43287  3lexlogpow2ineq1  43299  3lexlogpow2ineq2  43300  3lexlogpow5ineq5  43301  aks4d1p1p3  43310  aks4d1p1p2  43311  aks4d1p1p4  43312  aks4d1p1p5  43316  aks4d1p1  43317  aks4d1p3  43319  aks4d1p8  43328  posbezout  43341  primrootspoweq0  43347  aks6d1c1  43357  hashscontpow1  43362  aks6d1c4  43365  aks6d1c2  43371  aks6d1c5lem1  43377  aks6d1c5lem3  43378  aks6d1c5lem2  43379  deg1gprod  43381  sticksstones7  43393  sticksstones10  43396  sticksstones12  43399  sticksstones22  43409  aks6d1c6lem1  43411  aks6d1c6lem3  43413  aks6d1c6lem4  43414  bcled  43419  bcle2d  43420  aks6d1c7lem1  43421  unitscyglem4  43439  aks5lem7  43441  aks5  43445  explt1d  43571  mulgt0b2d  43733  evlselv  43808  dffltz  43861  fltnlta  43865  irrapxlem1  44020  pell1qrgaplem  44071  pell1qrgap  44072  monotoddzzfi  44140  jm2.24nn  44157  congtr  44163  congmul  44165  congsub  44168  fzmaxdif  44179  acongeq  44181  jm2.20nn  44195  jm2.25  44197  hbtlem4  44318  dgrsub2  44327  mpaaeu  44342  idomsubgmo  44385  iscard4  44724  sqrtcvallem4  44829  leeq2d  45348  int-sqgeq0d  45376  int-ineqmvtd  45381  cvgdvgrat  45487  radcnvrat  45488  hashnzfzclim  45496  dvconstbi  45508  binomcxplemdvbinom  45527  isosctrlem1ALT  46105  mulltgt0  46242  rnmptbd2lem  46463  oddfl  46497  2timesgt  46507  lt3addmuld  46520  lt4addmuld  46525  supxrgere  46548  supxrgelem  46552  supxrge  46553  xadd0ge2  46556  infrpge  46566  xrlexaddrp  46567  xralrple2  46569  infxr  46581  infleinflem1  46584  infleinflem2  46585  infleinf  46586  xralrple4  46587  xralrple3  46588  recnnltrp  46591  rpgtrecnn  46594  xrralrecnnge  46604  rexabslelem  46631  infrnmptle  46636  supminfxr  46677  xrpnf  46698  iccshift  46733  iooshift  46737  ressiocsup  46769  ressioosup  46770  fsumnncl  46787  fmul01  46795  fmul01lt1lem1  46799  fmul01lt1lem2  46800  mccllem  46812  climrec  46818  climexp  46820  climneg  46825  limcrecl  46844  sumnnodd  46845  lptioo2  46846  lptioo1  46847  ltmod  46851  lptre2pt  46853  0ellimcdiv  46862  limclner  46864  fnlimcnv  46880  climinf2lem  46919  limsupubuzlem  46925  limsup10exlem  46985  limsupgtlem  46990  dfxlim2v  47060  xlimliminflimsup  47075  cncficcgt0  47101  cncfioobdlem  47109  ioodvbdlimc1lem1  47144  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  dvdsn1add  47152  dvnxpaek  47155  dvnmul  47156  dvnprodlem1  47159  itgiccshift  47193  itgperiod  47194  sublevolico  47197  ismbl3  47199  ovolsplit  47201  ismbl4  47206  stoweidlem1  47214  stoweidlem11  47224  stoweidlem13  47226  stoweidlem26  47239  stoweidlem34  47247  stoweidlem38  47251  stoweidlem42  47255  stoweidlem51  47264  stoweidlem59  47272  stirlinglem5  47291  stirlinglem6  47292  stirlinglem7  47293  stirlinglem10  47296  stirlinglem11  47297  stirlinglem13  47299  stirlinglem15  47301  dirkercncflem1  47316  dirkercncflem4  47319  fourierdlem4  47324  fourierdlem10  47330  fourierdlem11  47331  fourierdlem15  47335  fourierdlem20  47340  fourierdlem25  47345  fourierdlem26  47346  fourierdlem30  47350  fourierdlem37  47357  fourierdlem39  47359  fourierdlem40  47360  fourierdlem41  47361  fourierdlem42  47362  fourierdlem44  47364  fourierdlem47  47366  fourierdlem48  47367  fourierdlem49  47368  fourierdlem50  47369  fourierdlem51  47370  fourierdlem52  47371  fourierdlem54  47373  fourierdlem60  47379  fourierdlem61  47380  fourierdlem63  47382  fourierdlem64  47383  fourierdlem65  47384  fourierdlem73  47392  fourierdlem74  47393  fourierdlem75  47394  fourierdlem76  47395  fourierdlem78  47397  fourierdlem79  47398  fourierdlem81  47400  fourierdlem84  47403  fourierdlem87  47406  fourierdlem92  47411  fourierdlem93  47412  fourierdlem101  47420  fourierdlem102  47421  fourierdlem103  47422  fourierdlem104  47423  fourierdlem111  47430  fourierdlem114  47433  sqwvfoura  47441  sqwvfourb  47442  fouriersw  47444  etransclem19  47466  etransclem23  47470  etransclem24  47471  etransclem25  47472  etransclem27  47474  etransclem32  47479  etransclem35  47482  etransclem48  47495  qndenserrnbllem  47507  ioorrnopnlem  47517  ioorrnopnxrlem  47519  fsumlesge0  47590  sge0cl  47594  sge0supre  47602  sge0less  47605  sge0gerp  47608  sge0ltfirp  47613  sge0le  47620  sge0ltfirpmpt  47621  sge0split  47622  sge0rpcpnf  47634  sge0ltfirpmpt2  47639  sge0isum  47640  sge0xaddlem1  47646  sge0pnffigtmpt  47653  sge0pnffsumgt  47655  sge0gtfsumgt  47656  sge0seq  47659  nnfoctbdjlem  47668  meassle  47676  meaiuninclem  47693  meaiininclem  47699  omeiunle  47730  omeiunltfirp  47732  carageniuncllem2  47735  carageniuncl  47736  omess0  47747  hoicvr  47761  ovnlerp  47775  ovnsubaddlem1  47783  hsphoidmvle2  47798  hoidmv1lelem2  47805  hoidmv1le  47807  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvlelem5  47812  ovnhoilem2  47815  ovnhoi  47816  hoidifhspdmvle  47833  hoiqssbllem2  47836  hspmbllem2  47840  hspmbllem3  47841  hspmbl  47842  vonioolem2  47894  vonicclem2  47897  smfaddlem1  47976  smflimlem2  47985  smflimlem4  47987  smfmullem1  48004  smfinflem  48030  smflimsuplem4  48036  smflimsuplem8  48040  chnsubseq  48093  sqrtnpoly  48146  perfectALTVlem2  49023  nnpw2blen  49895  itscnhlinecirc02plem1  50097  funcoppc3  50466  oppcuprcl2  50521  isinito3  50838