Theorem breqtrd 5136

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  breqtrrd  5138  breqtrid  5147  domunsn  9113  mapdom2  9134  phplem2  9187  mapfien2  9367  wemaplem2  9507  infdifsn  9624  cantnff  9641  ttrclss  9687  rnttrcl  9689  infxpenlem  10004  infmap2  10207  ssfin4  10300  canthp1lem1  10643  nqereq  10926  ltexnq  10966  ltbtwnnq  10969  add20  11732  mullt0  11739  ltm1  12063  recgt0  12067  prodgt0  12068  ltmul1a  12070  mulge0b  12091  recp1lt1  12119  recreclt  12120  ledivp1  12123  ledivp1i  12146  ltdivp1i  12147  eluzmn  12875  ltaddrp2d  13100  mul2lt0bi  13130  prodge0rd  13131  xleadd1a  13285  xov1plusxeqvd  13531  fz01en  13587  fzonmapblen  13744  fladdz  13865  flhalf  13870  fldiv  13900  modsubdir  13983  fzen2  14012  serle  14100  ltexp2a  14209  leexp2a  14215  exple1  14220  expubnd  14221  bernneq  14272  expmulnbnd  14278  discr1  14282  discr  14283  faclbnd6  14342  hashfz  14471  hashfun  14481  seqcoll  14508  sqeqd  15224  01sqrexlem7  15306  sqrtge0  15315  sqrtneglem  15324  abslt  15373  absle  15374  abstri  15389  rlimge0  15639  reccn2  15655  climaddc2  15694  isercolllem1  15723  caucvgrlem  15731  summolem2a  15773  isumge0  15824  fsumle  15858  fsumlt  15859  o1fsum  15872  supcvg  15917  expcnv  15925  geolim  15931  geolim2  15932  georeclim  15933  geo2lim  15936  mertenslem1  15945  mertens  15947  prodmolem2a  15995  efcllem  16137  ef0lem  16138  efgt0  16165  eftlub  16171  eflt  16179  sinbnd  16242  cosbnd  16243  ef01bndlem  16246  sin01gt0  16252  cos01gt0  16253  sin02gt0  16254  eirrlem  16266  rpnnen2lem11  16286  rpnnen2lem12  16287  ruclem11  16302  dvdssub2  16365  dvdsadd2b  16370  dvdsexp  16392  3dvds  16395  opoe  16427  bitsfzolem  16498  bitsinv1lem  16505  bezoutlem4  16606  dvdsgcd  16608  dvdsmulgcd  16620  bezoutr1  16633  nn0seqcvgd  16634  rpmulgcd2  16720  qredeq  16721  rpdvds  16724  prmind2  16749  divdenle  16814  hashdvds  16840  phimullem  16844  eulerthlem2  16847  prmdiveq  16851  prmdivdiv  16852  pythagtriplem4  16885  pythagtriplem10  16886  pythagtriplem19  16899  iserodd  16901  pcpre1  16908  pcadd2  16956  qexpz  16967  expnprm  16968  oddprmdvds  16969  pockthlem  16971  prmreclem2  16983  prmreclem3  16984  4sqlem7  17010  4sqlem10  17013  4sqlem11  17021  4sqlem12  17022  4sqlem14  17024  4sqlem15  17025  4sqlem16  17026  0ram  17086  ffthiso  17994  latmlej12  18541  qusgrp  19263  pgpfi1  19671  sylow1lem4  19677  sylow1lem5  19678  odcau  19680  pgpfi  19681  pgpssslw  19690  sylow3lem4  19706  sylow3lem6  19708  efgsfo  19815  frgp0  19836  odadd1  19924  odadd2  19925  odadd  19926  gexexlem  19928  lt6abl  19971  gsumzsubmcl  19994  pwsgsum  20058  dprd2dlem1  20119  dprd2d2  20122  ablfacrplem  20143  ablfacrp  20144  ablfacrp2  20145  ablfac1b  20148  ablfac1eu  20151  pgpfac1lem3a  20154  ablfaclem2  20164  dvdsrid  20456  dvdsrtr  20457  dvdsrneg  20459  unitmulcl  20469  unitgrp  20472  unitnegcl  20486  subrguss  20697  subrgunit  20700  isdrng2  20854  fidomndrnglem  20887  abvsubtri  20941  orngsqr  20980  ornglmulle  20981  orngrmulle  20982  orng0le1  20988  gzrngunit  21594  prmirredlem  21633  znidomb  21722  frlmgsum  21933  psrbaglesupp  22083  psdmul  22340  psdmvr  22343  invrvald  22844  psmetsym  24478  psmettri  24479  mettri2  24509  xmetsym  24515  xmettri  24519  prdsxmetlem  24536  xblss2ps  24569  xblss2  24570  blhalf  24573  xmsge0  24631  ngptgp  24804  nrginvrcnlem  24859  nmoeq0  24904  cnmet  24939  blcvx  24966  opnreen  25000  metdcnlem  25005  metdstri  25020  metdsle  25021  metnrmlem1  25028  metnrmlem3  25030  lebnumlem1  25131  pi1inv  25222  cphnmf  25365  ipge0  25368  ipcau2  25404  tcphcphlem1  25405  csbren  25569  minveclem2  25596  minveclem3  25599  ovolssnul  25657  ovolctb  25660  ovolunnul  25670  ovoliunlem1  25672  ovoliun2  25676  ovoliunnul  25677  ioombl1lem4  25731  uniioombllem3  25755  uniioombllem4  25756  uniioombllem5  25757  uniioombl  25759  volcn  25776  vitalilem2  25779  vitalilem5  25782  itg1lea  25882  mbfi1fseqlem6  25890  mbfi1flimlem  25892  itg2eqa  25915  itg2splitlem  25918  itg2split  25919  itg2monolem1  25920  itg2cnlem2  25932  iblabsr  26000  iblmulc2  26001  bddiblnc  26012  dveflem  26149  dvef  26150  dvferm2lem  26156  dvlip  26163  c1liplem1  26166  dveq0  26170  dvlt0  26175  dvivthlem1  26178  lhop1  26184  dvfsumle  26191  dvfsumlem4  26199  dvfsumrlim3  26203  dvfsum2  26204  ftc1a  26207  ftc1lem4  26209  deg1add  26271  ply1divex  26305  ply1rem  26334  fta1glem2  26337  fta1blem  26339  ig1pdvds  26348  plyeq0lem  26378  dgrcolem2  26442  plydivlem4  26468  plyrem  26477  fta1lem  26479  aalioulem3  26508  aaliou2b  26515  aaliou3lem3  26518  aaliou3lem8  26519  ulmcn  26573  ulmdvlem1  26574  itgulm  26582  pserulm  26596  pserdvlem2  26602  abelthlem2  26606  abelthlem5  26609  abelthlem6  26610  abelthlem7  26612  abelthlem8  26613  abelthlem9  26614  sinq12gt0  26683  sinq34lt0t  26685  cosq14gt0  26686  cosq14ge0  26687  cos02pilt1  26702  efif1olem3  26720  argimgt0  26788  argimlt0  26789  logneg2  26791  logcnlem3  26820  logcnlem4  26821  logtayllem  26835  logtayl2  26838  cxpsqrtlem  26878  cxpsqrt  26879  cxpaddlelem  26927  abscxpbnd  26929  zrtdvds  26935  rtprmirr  26936  loglesqrt  26937  ang180lem2  26986  atanlogaddlem  27089  atanlogsublem  27091  atantan  27099  atans2  27107  atantayl  27113  leibpi  27118  log2tlbnd  27121  birthdaylem2  27128  birthdaylem3  27129  cxp2limlem  27151  jensenlem2  27163  jensen  27164  logdiflbnd  27170  emcllem2  27172  emcllem4  27174  harmonicbnd4  27186  fsumharmonic  27187  lgamgulmlem2  27205  lgamgulm2  27211  lgambdd  27212  lgamucov  27213  lgamcvglem  27215  lgamcvg2  27230  gamcvg  27231  wilthlem3  27245  basellem1  27256  basellem3  27258  basellem4  27259  fsumdvdsdiaglem  27358  dvdsppwf1o  27361  mpodvdsmulf1o  27369  dvdsmulf1o  27371  chteq0  27384  chtub  27387  chpub  27395  logfacubnd  27396  logfaclbnd  27397  logexprlim  27400  perfectlem2  27405  dchrfi  27430  bclbnd  27455  bposlem1  27459  bposlem3  27461  bposlem4  27462  bposlem6  27464  lgslem1  27472  lgsqrlem2  27522  lgsqrlem4  27524  lgseisenlem2  27551  lgsquadlem1  27555  lgsquadlem2  27556  lgsquad2lem1  27559  2sqlem3  27595  2sqlem4  27596  2sqlem8  27601  2sqlem11  27604  2sqcoprm  27610  2sqmod  27611  chebbnd1lem2  27645  chebbnd1lem3  27646  chtppilimlem1  27648  chpchtlim  27654  vmadivsum  27657  vmadivsumb  27658  rpvmasumlem  27662  dchrisumlem2  27665  dchrmusum2  27669  dchrvmasumlem2  27673  dchrvmasumlem3  27674  dchrisum0flblem2  27684  dchrisum0fno1  27686  dchrisum0re  27688  dchrisum0lem1  27691  dchrisum0lem2a  27692  mudivsum  27705  mulogsumlem  27706  mulog2sumlem2  27710  vmalogdivsum2  27713  selberglem2  27721  selbergb  27724  selberg2b  27727  logdivbnd  27731  selberg3lem1  27732  selberg3lem2  27733  selberg4lem1  27735  pntrmax  27739  pntrlog2bndlem2  27753  pntrlog2bndlem3  27754  pntrlog2bndlem5  27756  pntrlog2bndlem6a  27757  pntrlog2bndlem6  27758  pntrlog2bnd  27759  pntpbnd1a  27760  pntpbnd1  27761  pntpbnd2  27762  pntibndlem1  27764  pntibndlem2  27766  pntlemb  27772  pntlemq  27776  pntlemr  27777  pntlemj  27778  pntlemk  27781  qabvle  27800  padicabvcxp  27807  ostth2lem2  27809  ostth2lem3  27810  ostth2lem4  27811  ostth3  27813  addsuniflem  28205  negsid  28245  negsunif  28259  negright  28263  mulsuniflem  28353  ltmuls2  28375  precsexlem9  28419  absmuls  28448  zcuts  28611  addhalfcut  28663  pw2cut2  28666  bdayfinbndlem1  28671  z12sge0  28687  legtrid  28871  legov3  28878  krippenlem  28978  mideulem2  29026  midex  29029  opphllem5  29043  opphllem6  29044  opphl  29046  lmieu  29104  lmiisolem  29116  perpeqlem  29161  prlnghpg  29207  perpprlng  29211  prlngsymquadlem  29224  quadcgrprlng  29227  tgaltai  29228  ttgcontlem1  29245  colinearalglem4  29270  axpaschlem  29301  axcontlem7  29331  nbfusgrlevtxm2  29739  clwlksndivn  30448  eucrct2eupth  30607  nvge0  31036  smcnlem  31060  nmoub3i  31136  nmoub2i  31137  nmlno0lem  31156  minvecolem2  31238  htthlem  31280  norm3dif2  31514  bcs2  31545  chscllem2  32001  eigposi  32199  nmopub2tALT  32272  nmfnleub2  32289  nmlnop0iALT  32358  riesz1  32428  cnlnadjlem2  32431  nmopcoadji  32464  leopsq  32492  leopmul  32497  leopnmid  32501  nmopleid  32502  opsqrlem6  32508  0leopj  32549  hstle1  32589  strlem3a  32615  mdslmd4i  32696  cvexchlem  32731  cdj1i  32796  unidifsnel  32892  unidifsnne  32893  le2halvesd  33112  xlt2addrd  33115  fsumub  33183  sgnmulsgp  33187  2exple2exp  33189  oexpled  33191  wrdt2ind  33282  xrge0tsmsd  33402  fzto1st1  33431  cycpmco2lem4  33458  cycpmco2lem6  33460  cyc3conja  33486  archiabllem1a  33520  archiabllem2a  33523  archiabllem2c  33524  rprmdvdsprod  33833  1arithidomlem1  33834  1arithidomlem2  33835  1arithidom  33836  ply1dg3rt0irred  33883  mplmulmvr  33938  mplvrpmrhm  33946  exsslsb  33996  fedgmullem1  34028  fedgmullem2  34029  fldsdrgfldext2  34061  fldextrspundgdvdslem  34079  fldextrspundgdvds  34080  fldext2rspun  34081  extdgfialglem2  34092  algextdeglem8  34123  rtelextdg2lem  34125  constrext2chnlem  34149  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  metideq  34292  metider  34293  sqsscirc1  34307  esummono  34453  esumpad2  34455  esumle  34457  esumlef  34461  esumcst  34462  esumrnmpt2  34467  esum2d  34492  aean  34643  dya2ub  34669  dya2icoseg  34676  omssubadd  34699  inelcarsg  34710  carsgsigalem  34714  carsggect  34717  carsgclctunlem2  34718  eulerpartlemb  34767  fibp1  34800  signsplypnf  34946  signsply0  34947  fdvposlt  34995  fdvposle  34997  reprgt  35017  logdivsqrle  35046  hgt750lemb  35052  hgt750leme  35054  tgoldbachgtde  35056  subfacval3  35689  sconnpht2  35738  sconnpi1  35739  resconn  35746  snmlff  35829  sinccvglem  36172  faclimlem2  36244  btwnouttr2  36522  weiunpo  37004  dnibndlem5  37099  dnibndlem7  37101  dnibndlem8  37102  dnibndlem9  37103  dnibndlem10  37104  dnibnd  37108  knoppcnlem4  37113  knoppcnlem9  37118  unbdqndv2lem1  37126  unbdqndv2lem2  37127  knoppndvlem11  37139  knoppndvlem12  37140  knoppndvlem14  37142  knoppndvlem15  37143  knoppndvlem17  37145  knoppndvlem18  37146  knoppndvlem19  37147  knoppndvlem21  37149  ltflcei  38287  poimirlem9  38308  poimirlem26  38325  poimirlem27  38326  poimirlem29  38328  heicant  38334  mblfinlem2  38337  mblfinlem3  38338  mblfinlem4  38339  volsupnfl  38344  itg2addnclem  38350  itg2addnclem3  38352  iblmulc2nc  38364  ftc1cnnclem  38370  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc2nc  38381  dvasin  38383  geomcau  38438  bfplem2  38502  rrncmslem  38511  rrnequiv  38514  lsatcvatlem  39851  islshpcv  39855  atlatmstc  40121  cvlsupr7  40150  cvrval3  40215  cvrval5  40217  cvrexchlem  40221  atcvrj1  40233  cvrat3  40244  cvrat4  40245  atbtwn  40248  1cvratex  40275  hlatexch4  40283  3atlem1  40285  3atlem2  40286  atcvrlln2  40321  atcvrlln  40322  lplnllnneN  40358  llncvrlpln2  40359  4atlem3b  40400  lplncvrlvol2  40417  dalemswapyz  40458  dalemswapyzps  40492  dalem25  40500  dalem39  40513  dalem58  40532  dalem59  40533  lneq2at  40580  lncvrat  40584  dalawlem2  40674  dalawlem3  40675  dalawlem4  40676  dalawlem6  40678  dalawlem9  40681  dalawlem11  40683  dalawlem12  40684  lhpocnle  40818  lhpmcvr3  40827  lhpmcvr5N  40829  lhpmcvr6N  40830  4atexlemunv  40868  4atexlemc  40871  4atexlemex2  40873  lautm  40896  cdlemc2  40994  cdleme5  41042  cdleme11j  41069  cdleme16b  41081  cdlemednpq  41101  cdleme19e  41109  cdleme20i  41119  cdleme22a  41142  cdleme22cN  41144  cdleme22d  41145  cdleme22e  41146  cdleme22eALTN  41147  cdleme22f  41148  cdleme23c  41153  cdleme30a  41180  cdleme35a  41250  cdleme35b  41252  cdleme42h  41284  cdlemeg46rgv  41330  cdlemg8b  41430  cdlemg12e  41449  cdlemg13a  41453  cdlemg17pq  41474  cdlemg18c  41482  cdlemg19  41486  cdlemg21  41488  cdlemg31d  41502  cdlemg33a  41508  tendoid  41575  cdlemk4  41636  cdlemki  41643  cdlemk10  41645  cdlemksv2  41649  cdlemk12  41652  cdlemk14  41656  cdlemk15  41657  cdlemk1u  41661  cdlemk5u  41663  cdlemk12u  41674  cdlemk45  41749  cdlemk48  41752  dia2dimlem1  41866  dia2dimlem2  41867  dia2dimlem3  41868  cdlemm10N  41920  cdlemn2  41997  dihjustlem  42018  dihglbcpreN  42102  dihmeetlem3N  42107  nnproddivdvdsd  42795  lcmineqlem17  42840  lcmineqlem18  42841  3lexlogpow2ineq1  42853  3lexlogpow2ineq2  42854  3lexlogpow5ineq5  42855  aks4d1p1p3  42864  aks4d1p1p2  42865  aks4d1p1p4  42866  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p3  42873  aks4d1p8  42882  posbezout  42895  primrootspoweq0  42901  aks6d1c1  42911  hashscontpow1  42916  aks6d1c4  42919  aks6d1c2  42925  aks6d1c5lem1  42931  aks6d1c5lem3  42932  aks6d1c5lem2  42933  deg1gprod  42935  sticksstones7  42947  sticksstones10  42950  sticksstones12  42953  sticksstones22  42963  aks6d1c6lem1  42965  aks6d1c6lem3  42967  aks6d1c6lem4  42968  bcled  42973  bcle2d  42974  aks6d1c7lem1  42975  unitscyglem4  42993  aks5lem7  42995  aks5  42999  explt1d  43112  mulgt0b2d  43280  evlselv  43349  dffltz  43394  fltdvdsabdvdsc  43398  fltaccoprm  43400  fltabcoprm  43402  flt4lem5elem  43411  flt4lem7  43419  fltnlta  43423  irrapxlem1  43577  pell1qrgaplem  43628  pell1qrgap  43629  monotoddzzfi  43697  jm2.24nn  43714  congtr  43720  congmul  43722  congsub  43725  fzmaxdif  43736  acongeq  43738  jm2.20nn  43752  jm2.25  43754  hbtlem4  43881  dgrsub2  43890  mpaaeu  43905  idomsubgmo  43948  iscard4  44287  sqrtcvallem4  44393  leeq2d  44912  int-sqgeq0d  44940  int-ineqmvtd  44945  cvgdvgrat  45051  radcnvrat  45052  hashnzfzclim  45060  dvconstbi  45072  binomcxplemdvbinom  45091  isosctrlem1ALT  45670  mulltgt0  45770  rnmptbd2lem  45991  oddfl  46025  2timesgt  46035  lt3addmuld  46048  lt4addmuld  46053  supxrgere  46077  supxrgelem  46081  supxrge  46082  xadd0ge2  46085  infrpge  46095  xrlexaddrp  46096  xralrple2  46098  infxr  46110  infleinflem1  46113  infleinflem2  46114  infleinf  46115  xralrple4  46116  xralrple3  46117  recnnltrp  46120  rpgtrecnn  46123  xrralrecnnge  46133  rexabslelem  46160  infrnmptle  46165  supminfxr  46206  xrpnf  46227  iccshift  46262  iooshift  46266  ressiocsup  46298  ressioosup  46299  fsumnncl  46316  fmul01  46324  fmul01lt1lem1  46328  fmul01lt1lem2  46329  mccllem  46341  climrec  46347  climexp  46349  climneg  46354  limcrecl  46373  sumnnodd  46374  lptioo2  46375  lptioo1  46376  ltmod  46380  lptre2pt  46382  0ellimcdiv  46391  limclner  46393  fnlimcnv  46409  climinf2lem  46448  limsupubuzlem  46454  limsup10exlem  46514  limsupgtlem  46519  dfxlim2v  46589  xlimliminflimsup  46604  cncficcgt0  46630  cncfioobdlem  46638  ioodvbdlimc1lem1  46673  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  dvdsn1add  46681  dvnxpaek  46684  dvnmul  46685  dvnprodlem1  46688  itgiccshift  46722  itgperiod  46723  sublevolico  46726  ismbl3  46728  ovolsplit  46730  ismbl4  46735  stoweidlem1  46743  stoweidlem11  46753  stoweidlem13  46755  stoweidlem26  46768  stoweidlem34  46776  stoweidlem38  46780  stoweidlem42  46784  stoweidlem51  46793  stoweidlem59  46801  stirlinglem5  46820  stirlinglem6  46821  stirlinglem7  46822  stirlinglem10  46825  stirlinglem11  46826  stirlinglem13  46828  stirlinglem15  46830  dirkercncflem1  46845  dirkercncflem4  46848  fourierdlem4  46853  fourierdlem10  46859  fourierdlem11  46860  fourierdlem15  46864  fourierdlem20  46869  fourierdlem25  46874  fourierdlem26  46875  fourierdlem30  46879  fourierdlem37  46886  fourierdlem39  46888  fourierdlem40  46889  fourierdlem41  46890  fourierdlem42  46891  fourierdlem44  46893  fourierdlem47  46895  fourierdlem48  46896  fourierdlem49  46897  fourierdlem50  46898  fourierdlem51  46899  fourierdlem52  46900  fourierdlem54  46902  fourierdlem60  46908  fourierdlem61  46909  fourierdlem63  46911  fourierdlem64  46912  fourierdlem65  46913  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem78  46926  fourierdlem79  46927  fourierdlem81  46929  fourierdlem84  46932  fourierdlem87  46935  fourierdlem92  46940  fourierdlem93  46941  fourierdlem101  46949  fourierdlem102  46950  fourierdlem103  46951  fourierdlem104  46952  fourierdlem111  46959  fourierdlem114  46962  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  etransclem19  46995  etransclem23  46999  etransclem24  47000  etransclem25  47001  etransclem27  47003  etransclem32  47008  etransclem35  47011  etransclem48  47024  qndenserrnbllem  47036  ioorrnopnlem  47046  ioorrnopnxrlem  47048  fsumlesge0  47119  sge0cl  47123  sge0supre  47131  sge0less  47134  sge0gerp  47137  sge0ltfirp  47142  sge0le  47149  sge0ltfirpmpt  47150  sge0split  47151  sge0rpcpnf  47163  sge0ltfirpmpt2  47168  sge0isum  47169  sge0xaddlem1  47175  sge0pnffigtmpt  47182  sge0pnffsumgt  47184  sge0gtfsumgt  47185  sge0seq  47188  nnfoctbdjlem  47197  meassle  47205  meaiuninclem  47222  meaiininclem  47228  omeiunle  47259  omeiunltfirp  47261  carageniuncllem2  47264  carageniuncl  47265  omess0  47276  hoicvr  47290  ovnlerp  47304  ovnsubaddlem1  47312  hsphoidmvle2  47327  hoidmv1lelem2  47334  hoidmv1le  47336  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvlelem5  47341  ovnhoilem2  47344  ovnhoi  47345  hoidifhspdmvle  47362  hoiqssbllem2  47365  hspmbllem2  47369  hspmbllem3  47370  hspmbl  47371  vonioolem2  47423  vonicclem2  47426  smfaddlem1  47505  smflimlem2  47514  smflimlem4  47516  smfmullem1  47533  smfinflem  47559  smflimsuplem4  47565  smflimsuplem8  47569  chnsubseq  47624  perfectALTVlem2  48515  nnpw2blen  49388  itscnhlinecirc02plem1  49590  funcoppc3  49953  oppcuprcl2  50008  isinito3  50306