Theorem rspcev 3552

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2139, ax-11 2156, ax-12 2173. (Revised by SN, 12-Dec-2023.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcev	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 481	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3544	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069

This theorem is referenced by:  rspceaimv  3557  rspc2ev  3564  rspc3ev  3566  rspceeqv  3567  reu6i  3658  rspesbca  3810  eliuni  4927  iuneqconst  4932  brralrspcev  5130  wefrc  5574  wereu2  5577  xpdifid  6060  frpomin  6228  onfr  6290  ordunidif  6299  eliman0  6791  dffv2  6845  elrnrexdm  6947  eldmrexrn  6949  elabrex  7098  f1elima  7117  fliftfun  7163  fliftval  7167  f1oiso2  7203  sorpssuni  7563  sorpssint  7564  onssmin  7619  onminex  7629  fimaproj  7947  tfrlem12  8191  seqomlem2  8252  oawordeulem  8347  oaass  8354  odi  8372  omass  8373  omeulem1  8375  oen0  8379  oelim2  8388  oeeulem  8394  nnawordex  8430  boxcutc  8687  snfi  8788  rexdif1en  8906  findcard  8908  nnfi  8912  pssnn  8913  ssnnfiOLD  8915  unfi  8917  pwfir  8921  onfin  8944  pssnnOLD  8969  dif1enALT  8980  frfi  8989  fisupg  8992  nnsdomg  9003  unfiOLD  9011  fissuni  9054  fipreima  9055  finsschain  9056  indexfi  9057  marypha1lem  9122  eqsup  9145  supmax  9156  fisup2g  9157  fisupcl  9158  supisoex  9163  infmin  9183  fiinfg  9188  fiinf2g  9189  wofib  9234  wemaplem2  9236  card2inf  9244  brwdom2  9262  cnfcom3clem  9393  trpredtr  9408  dftrpred3g  9412  trcl  9417  frmin  9438  r1ordg  9467  r1pwss  9473  tz9.12lem3  9478  tz9.12  9479  r1elwf  9485  tcrank  9573  scottex  9574  scott0  9575  isnumi  9635  onsdom  9685  ondomen  9724  infpwfien  9749  cardaleph  9776  infenaleph  9778  alephfplem4  9794  alephfp2  9796  dfac2b  9817  ackbij1lem18  9924  ackbij1  9925  cflem  9933  cflecard  9940  cfsuc  9944  cfflb  9946  cofsmo  9956  coftr  9960  fin23lem7  10003  fin23lem11  10004  enfin2i  10008  fin23lem26  10012  isf32lem5  10044  isf34lem4  10064  isfin1-3  10073  fin1a2lem7  10093  axdc3lem4  10140  ttukeylem7  10202  iunfo  10226  ficard  10252  pwcfsdom  10270  fpwwe2lem11  10328  wunex  10426  eltsk2g  10438  grur1  10507  axgroth6  10515  inaprc  10523  nqereu  10616  archnq  10667  genpnmax  10694  ltexpri  10730  prlem936  10734  recexpr  10738  supexpr  10741  negexsr  10789  recexsrlem  10790  recexsr  10794  supsrlem  10798  axrnegex  10849  axrrecex  10850  axpre-sup  10856  1re  10906  dedekind  11068  dedekindle  11069  cnegex  11086  cnegex2  11087  recex  11537  receu  11550  fiminre2  11853  cju  11899  nn2ge  11930  nominpos  12140  zdiv  12320  btwnz  12352  uzwo  12580  ublbneg  12602  lbzbi  12605  zsupss  12606  uzsupss  12609  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem4  12649  rpnnen1lem5  12650  z2ge  12861  qbtwnre  12862  qbtwnxr  12863  xralrple  12868  xrsupsslem  12970  xrinfmsslem  12971  supxrpnf  12981  icc0  13056  uzsup  13511  expnbnd  13875  expmulnbnd  13878  hashkf  13974  hashdom  14022  iswrdi  14149  rtrclreclem1  14696  rtrclreclem2  14698  rtrclreclem3  14699  01sqrex  14889  resqrex  14890  sqrtneg  14907  abs1m  14975  rexanuz  14985  rexuz3  14988  rexuzre  14992  sqreu  15000  o1lo1  15174  climconst  15180  rlimclim1  15182  climshftlem  15211  rlimo1  15254  lo1add  15264  lo1mul  15265  lo1le  15291  isercoll  15307  serf0  15320  zsum  15358  fsum  15360  fsumcvg3  15369  mertenslem1  15524  ntrivcvgn0  15538  ntrivcvgmullem  15541  zprod  15575  fprod  15579  fprodntriv  15580  dvdsval2  15894  dvds0lem  15904  dvds1lem  15905  dvds2lem  15906  odd2np1lem  15977  odd2np1  15978  opeo  16002  omeo  16003  divalglem9  16038  gcdcllem3  16136  lcmcllem  16229  qredeu  16291  exprmfct  16337  isprm5  16340  odzcllem  16421  reumodprminv  16433  modprm0  16434  nnnn0modprm0  16435  pythagtriplem19  16462  pcprmpw2  16511  pockthi  16536  infpnlem2  16540  vdwlem2  16611  vdwlem10  16619  vdwlem13  16622  ramub1lem1  16655  cshwrepswhash1  16732  imasleval  17169  mreexexlem3d  17272  mreexexlem4d  17273  iscatd  17299  cat1  17728  poslubd  18046  fpwipodrs  18173  ismgmid2  18267  mgmidsssn0  18271  gsumval2a  18284  ismndd  18322  isgrpd2  18514  isgrpd  18516  imasgrp2  18605  mhmmnd  18612  ghmgrp  18614  gaorber  18829  orbsta  18834  cayleyth  18938  pmtrdifel  19003  pmtrdifwrdel  19008  pmtrdifwrdel2  19009  psgnunilem2  19018  psgnunilem3  19019  psgnvalii  19032  pgpfi1  19115  sylow1lem3  19120  sylow1lem5  19122  pgpfi  19125  sylow2alem2  19138  efgredeu  19273  lt6abl  19411  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem5  19597  pgpfaclem1  19599  pgpfaclem3  19601  ablfaclem2  19604  dvdsrmul  19805  dvdsr01  19812  irredrmul  19864  lspf  20151  lspval  20152  lssats2  20177  lspfixed  20305  lspsolvlem  20319  zringlpir  20601  zncyg  20668  cygth  20691  frlmup4  20918  aspval  20987  evlseu  21203  fiinbas  22010  topbas  22030  pptbas  22066  clsval  22096  elcls  22132  neiint  22163  neips  22172  opnneissb  22173  opnssneib  22174  innei  22184  neiptopnei  22191  restbas  22217  neitr  22239  pnfnei  22279  mnfnei  22280  lmconst  22320  iscnp4  22322  cncnpi  22337  cnconst2  22342  cnprest  22348  cnpdis  22352  nrmsep  22416  regsep2  22435  cmpcovf  22450  cmpsub  22459  cmpcld  22461  hauscmplem  22465  conncompid  22490  2ndci  22507  2ndcsb  22508  2ndc1stc  22510  1stcrest  22512  2ndcctbss  22514  2ndcdisj  22515  2ndcomap  22517  2ndcsep  22518  dis2ndc  22519  restlly  22542  islly2  22543  hausllycmp  22553  cldllycmp  22554  lly1stc  22555  dislly  22556  ssref  22571  refref  22572  finlocfin  22579  dissnlocfin  22588  locfindis  22589  llycmpkgen2  22609  cmpkgen  22610  1stckgenlem  22612  elptr  22632  ptbasfi  22640  neitx  22666  ptpjopn  22671  txcnp  22679  ptcnplem  22680  txlly  22695  txnlly  22696  txtube  22699  txcmplem1  22700  tx1stc  22709  txkgen  22711  xkococnlem  22718  txconn  22748  tgqtop  22771  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  reghmph  22852  nrmhmph  22853  fbssfi  22896  opnfbas  22901  isfil2  22915  fsubbas  22926  ssfg  22931  fgss2  22933  fbasrn  22943  filuni  22944  fgtr  22949  ssufl  22977  uffix  22980  elfm2  23007  elfm3  23009  imaelfm  23010  rnelfmlem  23011  rnelfm  23012  fmfnfmlem4  23016  fmfnfm  23017  fmco  23020  ufldom  23021  hausflim  23040  flimcls  23044  hauspwpwf1  23046  flffbas  23054  txflf  23065  fclscf  23084  fclsfnflim  23086  alexsubALTlem4  23109  alexsubALT  23110  tmdgsum2  23155  symgtgp  23165  subgntr  23166  opnsubg  23167  ghmcnp  23174  qustgpopn  23179  tsmsfbas  23187  tsmsxplem1  23212  ustexsym  23275  elrnust  23284  trust  23289  utoptop  23294  restutop  23297  restutopopn  23298  ustuqtop4  23304  utopsnneiplem  23307  iducn  23343  fmucnd  23352  cfilufg  23353  trcfilu  23354  neipcfilu  23356  imasdsf1olem  23434  blssps  23485  blss  23486  blssexps  23487  blssex  23488  ssblex  23489  blin2  23490  neibl  23563  blcld  23567  metss2  23574  stdbdmopn  23580  met1stc  23583  met2ndci  23584  metrest  23586  prdsxmslem2  23591  metcnp3  23602  metuval  23611  metustexhalf  23618  metustfbas  23619  cfilucfil  23621  restmetu  23632  dscopn  23635  ngptgp  23698  nlmvscnlem1  23756  tgioo  23865  tgqioo  23869  xrsmopn  23881  zcld  23882  recld2  23883  zdis  23885  icccmplem1  23891  icccmplem2  23892  xmetdcn2  23906  addcnlem  23933  xrhmeo  24015  cnheibor  24024  cnllycmp  24025  lebnumlem3  24032  lebnum  24033  xlebnum  24034  lebnumii  24035  elpi1i  24115  ipcnlem1  24314  lmnn  24332  iscfil3  24342  cfilres  24365  flimcfil  24383  bcthlem4  24396  bcthlem5  24397  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem3  24498  minveclem4  24501  minveclem6  24503  ivthlem2  24521  ivth  24523  ivthle  24525  ivthle2  24526  elovolmr  24545  ovolunlem1  24566  ovoliunlem2  24572  ovolicc1  24585  iundisj  24617  iunmbl2  24626  dyadmbllem  24668  volivth  24676  mbflimsup  24735  i1faddlem  24762  i1fmullem  24763  itg2lr  24800  itg2monolem1  24820  limcnlp  24947  ellimc3  24948  limcflf  24950  limciun  24963  rollelem  25058  c1lip1  25066  lhop1lem  25082  ply1divex  25206  ig1peu  25241  elply2  25262  coeeq  25293  plydivlem3  25360  plydivlem4  25361  elqaalem3  25386  qaa  25388  iaa  25390  aareccl  25391  aannenlem2  25394  aalioulem2  25398  aalioulem3  25399  aalioulem5  25401  aalioulem6  25402  aaliou  25403  aaliou2  25405  aaliou3lem8  25410  ulmshftlem  25453  reeff1o  25511  pilem2  25516  pilem3  25517  efif1olem2  25604  efopn  25718  cxpcn3lem  25805  cxpeq  25815  dcubic2  25899  quart  25916  xrlimcnp  26023  ftalem5  26131  ftalem7  26133  sgmnncl  26201  dvdsppwf1o  26240  musum  26245  perfect  26284  dchrptlem1  26317  dchrptlem2  26318  dchrpt  26320  bpos1lem  26335  lgsqrlem4  26402  lgsdchrval  26407  2sqblem  26484  dchrisumlem3  26544  chpdifbndlem2  26607  pntrsumbnd2  26620  pntpbnd1  26639  pntpbnd2  26640  pntpbnd  26641  pntibndlem2  26644  pntibndlem3  26645  pntleme  26661  pntlem3  26662  axtgcont  26734  tgcgrxfr  26783  legid  26852  btwnleg  26853  leg0  26857  tghilberti1  26902  tglnpt2  26906  colline  26914  mirreu3  26919  isperp2  26980  colperpex  26998  lnopp2hpgb  27028  hpgerlem  27030  brbtwn  27170  brcgr  27171  brbtwn2  27176  axpasch  27212  axlowdimlem14  27226  axlowdim2  27231  axcontlem2  27236  axcontlem4  27238  axcontlem8  27242  axcontlem10  27244  axcontlem12  27246  fusgrn0degnn0  27769  friendshipgt3  28663  lpni  28743  isgrpoi  28761  vacn  28957  smcnlem  28960  nmosetn0  29028  nmoolb  29034  nmobndi  29038  nmoo0  29054  nmlno0lem  29056  isblo3i  29064  blo3i  29065  blocnilem  29067  ubthlem1  29133  minvecolem2  29138  minvecolem3  29139  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  norm1exi  29513  occl  29567  spanval  29596  spancl  29599  shsval2i  29650  ococin  29671  pjoml6i  29852  nmopsetn0  30128  nmfnsetn0  30141  nmoplb  30170  nmfnlb  30187  nmop0  30249  nmfn0  30250  nmlnop0iALT  30258  nmopun  30277  nmcexi  30289  lnconi  30296  lnopcnbd  30299  lnfncnbd  30320  riesz3i  30325  riesz1  30328  cnlnadjlem2  30331  cnlnadjlem8  30337  cnlnadjlem9  30338  adjbd1o  30348  branmfn  30368  opsqrlem1  30403  pjnmopi  30411  strlem1  30513  stri  30520  hstri  30528  cvcon3  30547  cvnbtwn  30549  superpos  30617  shatomici  30621  atcvat4i  30660  mdsymlem2  30667  cdj1i  30696  cdj3i  30704  rexunirn  30741  foresf1o  30751  iundisjf  30829  elunirn2  30890  aciunf1lem  30901  fnpreimac  30910  fgreu  30911  fcnvgreu  30912  xrge0infss  30985  ssnnssfz  31010  iundisjfi  31019  xreceu  31098  rexdiv  31102  isarchi3  31343  archirngz  31345  archiabllem2a  31350  rhmdvdsr  31419  0nellinds  31468  qtophaus  31688  reff  31691  locfinreflem  31692  cmpcref  31702  dispcmp  31711  metidval  31742  pstmval  31747  tpr2rico  31764  pnfneige0  31803  qqhucn  31842  rrhre  31871  indf1ofs  31894  esumcst  31931  esumpcvgval  31946  dmsigagen  32012  rossros  32048  dya2icoseg  32144  dya2iocnrect  32148  dya2iocuni  32150  eulerpartlemgvv  32243  dstfrvunirn  32341  ballotlem4  32365  ballotlemic  32373  ballotlem1c  32374  ballotlemrc  32397  signsw0g  32435  signswmnd  32436  prodfzo03  32483  tgoldbachgt  32543  loop1cycl  32999  umgr2cycllem  33002  umgr2cycl  33003  subfacp1lem3  33044  erdsze2lem2  33066  cnpconn  33092  txpconn  33094  ptpconn  33095  indispconn  33096  connpconn  33097  cvxpconn  33104  cnllysconn  33107  cvmsss2  33136  cvmcov2  33137  cvmopnlem  33140  cvmliftlem14  33159  cvmliftlem15  33160  cvmlift2lem11  33175  cvmlift2lem12  33176  cvmlift2lem13  33177  cvmlift3lem2  33182  cvmlift3lem6  33186  cvmlift3lem9  33189  mthmi  33439  onelssex  33563  eldifsucnn  33597  br8  33629  br6  33630  br4  33631  dfon2lem9  33673  ssttrcl  33701  ttrcltr  33702  frxp2  33718  frxp3  33724  poseq  33729  wzel  33745  wsuclem  33746  wsuclb  33749  naddcllem  33758  elno2  33784  sltval2  33786  noreson  33790  sltres  33792  noseponlem  33794  nolesgn2o  33801  nogesgn1o  33803  nodense  33822  nosupfv  33836  nosupres  33837  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2lem1  33860  noetasuplem4  33866  noetainflem4  33870  noetalem2  33872  oldlim  33996  cofcutrtime  34020  imagesset  34182  fvtransport  34261  brcolinear  34288  brsegle  34337  seglerflx  34341  seglemin  34342  btwnsegle  34346  fvray  34370  fvline  34373  hilbert1.1  34383  elhf2  34404  0hf  34406  nn0prpwlem  34438  nn0prpw  34439  fness  34465  fneref  34466  fnessref  34473  refssfne  34474  neibastop2lem  34476  fnemeet1  34482  tailfb  34493  filnetlem4  34497  limsucncmpi  34561  taupilemrplb  35418  relowlssretop  35461  rdgellim  35474  matunitlindflem2  35701  ptrecube  35704  poimirlem4  35708  poimirlem17  35721  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem32  35736  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  volsupnfl  35749  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  ftc1anclem5  35781  unirep  35798  cover2  35799  indexa  35818  frinfm  35820  sdclem1  35828  fdc  35830  incsequz  35833  caushft  35846  istotbnd3  35856  0totbnd  35858  sstotbnd2  35859  sstotbnd  35860  sstotbnd3  35861  isbnd3  35869  ssbnd  35873  equivbnd  35875  prdsbnd  35878  prdstotbnd  35879  cntotbnd  35881  heibor1lem  35894  heiborlem1  35896  heiborlem3  35898  heiborlem6  35901  heiborlem8  35903  bfplem2  35908  rrncmslem  35917  iccbnd  35925  opidonOLD  35937  exidres  35963  isrngod  35983  isgrpda  36040  isdrngo2  36043  igenval  36146  igenidl  36148  prtlem10  36806  lshpnel2N  36926  lsmsat  36949  lssatomic  36952  lcvnbtwn  36966  lfl1  37011  eqlkr  37040  lshpkrlem1  37051  lshpkrex  37059  cvrcon3b  37218  cvrat4  37384  3dim3  37410  ps-2  37419  llni  37449  llnle  37459  lplni  37473  lplnle  37481  lplnexllnN  37505  lvoli  37516  lnatexN  37720  elpaddn0  37741  pclfinN  37841  lhprelat3N  37981  4atexlemex2  38012  4atex  38017  4atex2-0aOLDN  38019  4atex2-0cOLDN  38021  lautcvr  38033  cdleme0ex1N  38164  cdleme50rnlem  38485  cdleme50ex  38500  cdlemg1cex  38529  cdlemkid5  38876  cdlemk  38915  tendoex  38916  cdleml5N  38921  cdlemm10N  39059  dih1dimatlem0  39269  dihjat1lem  39369  dvh3dim2  39389  dvh3dim3N  39390  dochkr1  39419  dochkr1OLDN  39420  lcfrvalsnN  39482  lcfrlem27  39510  lcfrlem37  39520  lcfr  39526  mapd1o  39589  mapdpglem23  39635  hdmap11lem2  39783  rspcedvdw  40107  resubeu  40281  nacsfix  40450  mzpcompact2lem  40489  eldioph  40496  diophrw  40497  diophin  40510  rexrabdioph  40532  rexzrexnn0  40542  eldioph4b  40549  rencldnfilem  40558  irrapxlem5  40564  irrapxlem6  40565  pell1234qrdich  40599  pell14qrdich  40607  infmrgelbi  40616  pellqrex  40617  pellfundre  40619  pellfundlb  40622  rmxynorm  40656  congrep  40711  acongrep  40718  jm2.27  40746  fnwe2lem2  40792  islssfgi  40813  hbtlem2  40865  hbtlem4  40867  hbtlem5  40869  dgraaub  40889  mpaaeu  40891  aaitgo  40903  rgspnval  40909  rgspncl  40910  clsk1independent  41545  elabrexg  42478  restuni3  42556  iinssd  42569  founiiun  42604  wessf1ornlem  42611  founiiun0  42617  unirnmap  42637  dstregt0  42709  uzfissfz  42755  rpgtrecnn  42809  rexabslelem  42848  infrnmptle  42853  infxrunb3rnmpt  42858  infxrpnf  42876  supminfxr  42894  iooiinicc  42970  iooiinioc  42984  uzubioo  42995  climsuse  43039  islptre  43050  limsuppnfdlem  43132  climinf3  43147  limsupmnfuzlem  43157  limsupre3lem  43163  limsupre3uzlem  43166  0cnv  43173  liminfreuzlem  43233  cnrefiisplem  43260  icccncfext  43318  cncficcgt0  43319  dvbdfbdioo  43361  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem9  43440  stoweidlem14  43445  stoweidlem18  43449  stoweidlem21  43452  stoweidlem29  43460  stoweidlem34  43465  stoweidlem35  43466  stoweidlem39  43470  stoweidlem41  43472  stoweidlem45  43476  stoweidlem52  43483  stoweidlem55  43486  stoweidlem57  43488  stoweidlem60  43491  stirlinglem5  43509  stirlinglem13  43517  stirlinglem14  43518  fourierdlem16  43554  fourierdlem20  43558  fourierdlem21  43559  fourierdlem22  43560  fourierdlem25  43563  fourierdlem31  43569  fourierdlem39  43577  fourierdlem41  43579  fourierdlem42  43580  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem77  43614  fourierdlem81  43618  fourierdlem83  43620  fourierdlem103  43640  fourierdlem104  43641  elaa2lem  43664  etransclem47  43712  qndenserrnbl  43726  ioorrnopnlem  43735  ioorrnopnxrlem  43737  intsaluni  43758  salgencntex  43772  subsaliuncllem  43786  sge0resplit  43834  sge0seq  43874  sge0reuz  43875  nnfoctbdjlem  43883  meaiininclem  43914  hoicvrrex  43984  ovnlecvr  43986  ovnlerp  43990  hoidmv1lelem2  44020  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  ovnlecvr2  44038  hoiqssbl  44053  ovolval4lem2  44078  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  iinhoiicclem  44101  smfinflem  44237  smflimsuplem7  44246  sprsymrelfolem2  44833  perfectALTV  45063  9gbo  45114  11gbo  45115  nnsum3primes4  45128  nnsum3primesprm  45130  ssnn0ssfz  45573  lincsumcl  45660  lincscmcl  45661  zlmodzxzldep  45733  ldepsnlinc  45737  line2ylem  45985  line2xlem  45987  rspceb2dv  46036  sepfsepc  46109  lubsscl  46142  glbsscl  46143  aacllem  46391