Theorem rspcev 3537

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2141, ax-11 2158, ax-12 2175. (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 485	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3530	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 410	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067

This theorem is referenced by:  rspceaimv  3542  rspc2ev  3549  rspc3ev  3551  rspceeqv  3552  reu6i  3641  rspesbca  3793  eliuni  4910  iuneqconst  4915  brralrspcev  5113  wefrc  5545  wereu2  5548  xpdifid  6031  frpomin  6194  onfr  6252  ordunidif  6261  eliman0  6752  dffv2  6806  elrnrexdm  6908  eldmrexrn  6910  elabrex  7056  f1elima  7075  fliftfun  7121  fliftval  7125  f1oiso2  7161  sorpssuni  7520  sorpssint  7521  onssmin  7576  onminex  7586  fimaproj  7902  tfrlem12  8125  seqomlem2  8187  oawordeulem  8282  oaass  8289  odi  8307  omass  8308  omeulem1  8310  oen0  8314  oelim2  8323  oeeulem  8329  nnawordex  8365  boxcutc  8622  snfi  8721  rexdif1en  8839  findcard  8841  nnfi  8845  pssnn  8846  ssnnfiOLD  8848  unfi  8850  pwfir  8854  onfin  8870  pssnnOLD  8895  dif1enALT  8907  frfi  8916  fisupg  8919  nnsdomg  8930  unfiOLD  8938  fissuni  8981  fipreima  8982  finsschain  8983  indexfi  8984  marypha1lem  9049  eqsup  9072  supmax  9083  fisup2g  9084  fisupcl  9085  supisoex  9090  infmin  9110  fiinfg  9115  fiinf2g  9116  wofib  9161  wemaplem2  9163  card2inf  9171  brwdom2  9189  cnfcom3clem  9320  trpredtr  9335  dftrpred3g  9339  trcl  9344  frmin  9365  r1ordg  9394  r1pwss  9400  tz9.12lem3  9405  tz9.12  9406  r1elwf  9412  tcrank  9500  scottex  9501  scott0  9502  isnumi  9562  onsdom  9612  ondomen  9651  infpwfien  9676  cardaleph  9703  infenaleph  9705  alephfplem4  9721  alephfp2  9723  dfac2b  9744  ackbij1lem18  9851  ackbij1  9852  cflem  9860  cflecard  9867  cfsuc  9871  cfflb  9873  cofsmo  9883  coftr  9887  fin23lem7  9930  fin23lem11  9931  enfin2i  9935  fin23lem26  9939  isf32lem5  9971  isf34lem4  9991  isfin1-3  10000  fin1a2lem7  10020  axdc3lem4  10067  ttukeylem7  10129  iunfo  10153  ficard  10179  pwcfsdom  10197  fpwwe2lem11  10255  wunex  10353  eltsk2g  10365  grur1  10434  axgroth6  10442  inaprc  10450  nqereu  10543  archnq  10594  genpnmax  10621  ltexpri  10657  prlem936  10661  recexpr  10665  supexpr  10668  negexsr  10716  recexsrlem  10717  recexsr  10721  supsrlem  10725  axrnegex  10776  axrrecex  10777  axpre-sup  10783  1re  10833  dedekind  10995  dedekindle  10996  cnegex  11013  cnegex2  11014  recex  11464  receu  11477  fiminre2  11780  cju  11826  nn2ge  11857  nominpos  12067  zdiv  12247  btwnz  12279  uzwo  12507  ublbneg  12529  lbzbi  12532  zsupss  12533  uzsupss  12536  rpnnen1lem1  12574  rpnnen1lem3  12575  rpnnen1lem4  12576  rpnnen1lem5  12577  z2ge  12788  qbtwnre  12789  qbtwnxr  12790  xralrple  12795  xrsupsslem  12897  xrinfmsslem  12898  supxrpnf  12908  icc0  12983  uzsup  13436  expnbnd  13799  expmulnbnd  13802  hashkf  13898  hashdom  13946  iswrdi  14073  rtrclreclem1  14620  rtrclreclem2  14622  rtrclreclem3  14623  01sqrex  14813  resqrex  14814  sqrtneg  14831  abs1m  14899  rexanuz  14909  rexuz3  14912  rexuzre  14916  sqreu  14924  o1lo1  15098  climconst  15104  rlimclim1  15106  climshftlem  15135  rlimo1  15178  lo1add  15188  lo1mul  15189  lo1le  15215  isercoll  15231  serf0  15244  zsum  15282  fsum  15284  fsumcvg3  15293  mertenslem1  15448  ntrivcvgn0  15462  ntrivcvgmullem  15465  zprod  15499  fprod  15503  fprodntriv  15504  dvdsval2  15818  dvds0lem  15828  dvds1lem  15829  dvds2lem  15830  odd2np1lem  15901  odd2np1  15902  opeo  15926  omeo  15927  divalglem9  15962  gcdcllem3  16060  lcmcllem  16153  qredeu  16215  exprmfct  16261  isprm5  16264  odzcllem  16345  reumodprminv  16357  modprm0  16358  nnnn0modprm0  16359  pythagtriplem19  16386  pcprmpw2  16435  pockthi  16460  infpnlem2  16464  vdwlem2  16535  vdwlem10  16543  vdwlem13  16546  ramub1lem1  16579  cshwrepswhash1  16656  imasleval  17046  mreexexlem3d  17149  mreexexlem4d  17150  iscatd  17176  cat1  17603  poslubd  17919  fpwipodrs  18046  ismgmid2  18140  mgmidsssn0  18144  gsumval2a  18157  ismndd  18195  isgrpd2  18387  isgrpd  18389  imasgrp2  18478  mhmmnd  18485  ghmgrp  18487  gaorber  18702  orbsta  18707  cayleyth  18807  pmtrdifel  18872  pmtrdifwrdel  18877  pmtrdifwrdel2  18878  psgnunilem2  18887  psgnunilem3  18888  psgnvalii  18901  pgpfi1  18984  sylow1lem3  18989  sylow1lem5  18991  pgpfi  18994  sylow2alem2  19007  efgredeu  19142  lt6abl  19280  pgpfac1lem3a  19463  pgpfac1lem3  19464  pgpfac1lem5  19466  pgpfaclem1  19468  pgpfaclem3  19470  ablfaclem2  19473  dvdsrmul  19666  dvdsr01  19673  irredrmul  19725  lspf  20011  lspval  20012  lssats2  20037  lspfixed  20165  lspsolvlem  20179  zringlpir  20454  zncyg  20513  cygth  20536  frlmup4  20763  aspval  20832  evlseu  21043  fiinbas  21849  topbas  21869  pptbas  21905  clsval  21934  elcls  21970  neiint  22001  neips  22010  opnneissb  22011  opnssneib  22012  innei  22022  neiptopnei  22029  restbas  22055  neitr  22077  pnfnei  22117  mnfnei  22118  lmconst  22158  iscnp4  22160  cncnpi  22175  cnconst2  22180  cnprest  22186  cnpdis  22190  nrmsep  22254  regsep2  22273  cmpcovf  22288  cmpsub  22297  cmpcld  22299  hauscmplem  22303  conncompid  22328  2ndci  22345  2ndcsb  22346  2ndc1stc  22348  1stcrest  22350  2ndcctbss  22352  2ndcdisj  22353  2ndcomap  22355  2ndcsep  22356  dis2ndc  22357  restlly  22380  islly2  22381  hausllycmp  22391  cldllycmp  22392  lly1stc  22393  dislly  22394  ssref  22409  refref  22410  finlocfin  22417  dissnlocfin  22426  locfindis  22427  llycmpkgen2  22447  cmpkgen  22448  1stckgenlem  22450  elptr  22470  ptbasfi  22478  neitx  22504  ptpjopn  22509  txcnp  22517  ptcnplem  22518  txlly  22533  txnlly  22534  txtube  22537  txcmplem1  22538  tx1stc  22547  txkgen  22549  xkococnlem  22556  txconn  22586  tgqtop  22609  kqreglem1  22638  kqreglem2  22639  kqnrmlem1  22640  kqnrmlem2  22641  reghmph  22690  nrmhmph  22691  fbssfi  22734  opnfbas  22739  isfil2  22753  fsubbas  22764  ssfg  22769  fgss2  22771  fbasrn  22781  filuni  22782  fgtr  22787  ssufl  22815  uffix  22818  elfm2  22845  elfm3  22847  imaelfm  22848  rnelfmlem  22849  rnelfm  22850  fmfnfmlem4  22854  fmfnfm  22855  fmco  22858  ufldom  22859  hausflim  22878  flimcls  22882  hauspwpwf1  22884  flffbas  22892  txflf  22903  fclscf  22922  fclsfnflim  22924  alexsubALTlem4  22947  alexsubALT  22948  tmdgsum2  22993  symgtgp  23003  subgntr  23004  opnsubg  23005  ghmcnp  23012  qustgpopn  23017  tsmsfbas  23025  tsmsxplem1  23050  ustexsym  23113  elrnust  23122  trust  23127  utoptop  23132  restutop  23135  restutopopn  23136  ustuqtop4  23142  utopsnneiplem  23145  iducn  23180  fmucnd  23189  cfilufg  23190  trcfilu  23191  neipcfilu  23193  imasdsf1olem  23271  blssps  23322  blss  23323  blssexps  23324  blssex  23325  ssblex  23326  blin2  23327  neibl  23399  blcld  23403  metss2  23410  stdbdmopn  23416  met1stc  23419  met2ndci  23420  metrest  23422  prdsxmslem2  23427  metcnp3  23438  metuval  23447  metustexhalf  23454  metustfbas  23455  cfilucfil  23457  restmetu  23468  dscopn  23471  ngptgp  23534  nlmvscnlem1  23584  tgioo  23693  tgqioo  23697  xrsmopn  23709  zcld  23710  recld2  23711  zdis  23713  icccmplem1  23719  icccmplem2  23720  xmetdcn2  23734  addcnlem  23761  xrhmeo  23843  cnheibor  23852  cnllycmp  23853  lebnumlem3  23860  lebnum  23861  xlebnum  23862  lebnumii  23863  elpi1i  23943  ipcnlem1  24142  lmnn  24160  iscfil3  24170  cfilres  24193  flimcfil  24211  bcthlem4  24224  bcthlem5  24225  minveclem4c  24322  minveclem2  24323  minveclem3b  24325  minveclem3  24326  minveclem4  24329  minveclem6  24331  ivthlem2  24349  ivth  24351  ivthle  24353  ivthle2  24354  elovolmr  24373  ovolunlem1  24394  ovoliunlem2  24400  ovolicc1  24413  iundisj  24445  iunmbl2  24454  dyadmbllem  24496  volivth  24504  mbflimsup  24563  i1faddlem  24590  i1fmullem  24591  itg2lr  24628  itg2monolem1  24648  limcnlp  24775  ellimc3  24776  limcflf  24778  limciun  24791  rollelem  24886  c1lip1  24894  lhop1lem  24910  ply1divex  25034  ig1peu  25069  elply2  25090  coeeq  25121  plydivlem3  25188  plydivlem4  25189  elqaalem3  25214  qaa  25216  iaa  25218  aareccl  25219  aannenlem2  25222  aalioulem2  25226  aalioulem3  25227  aalioulem5  25229  aalioulem6  25230  aaliou  25231  aaliou2  25233  aaliou3lem8  25238  ulmshftlem  25281  reeff1o  25339  pilem2  25344  pilem3  25345  efif1olem2  25432  efopn  25546  cxpcn3lem  25633  cxpeq  25643  dcubic2  25727  quart  25744  xrlimcnp  25851  ftalem5  25959  ftalem7  25961  sgmnncl  26029  dvdsppwf1o  26068  musum  26073  perfect  26112  dchrptlem1  26145  dchrptlem2  26146  dchrpt  26148  bpos1lem  26163  lgsqrlem4  26230  lgsdchrval  26235  2sqblem  26312  dchrisumlem3  26372  chpdifbndlem2  26435  pntrsumbnd2  26448  pntpbnd1  26467  pntpbnd2  26468  pntpbnd  26469  pntibndlem2  26472  pntibndlem3  26473  pntleme  26489  pntlem3  26490  axtgcont  26560  tgcgrxfr  26609  legid  26678  btwnleg  26679  leg0  26683  tghilberti1  26728  tglnpt2  26732  colline  26740  mirreu3  26745  isperp2  26806  colperpex  26824  lnopp2hpgb  26854  hpgerlem  26856  brbtwn  26990  brcgr  26991  brbtwn2  26996  axpasch  27032  axlowdimlem14  27046  axlowdim2  27051  axcontlem2  27056  axcontlem4  27058  axcontlem8  27062  axcontlem10  27064  axcontlem12  27066  fusgrn0degnn0  27587  friendshipgt3  28481  lpni  28561  isgrpoi  28579  vacn  28775  smcnlem  28778  nmosetn0  28846  nmoolb  28852  nmobndi  28856  nmoo0  28872  nmlno0lem  28874  isblo3i  28882  blo3i  28883  blocnilem  28885  ubthlem1  28951  minvecolem2  28956  minvecolem3  28957  minvecolem4c  28960  minvecolem4  28961  minvecolem5  28962  minvecolem6  28963  norm1exi  29331  occl  29385  spanval  29414  spancl  29417  shsval2i  29468  ococin  29489  pjoml6i  29670  nmopsetn0  29946  nmfnsetn0  29959  nmoplb  29988  nmfnlb  30005  nmop0  30067  nmfn0  30068  nmlnop0iALT  30076  nmopun  30095  nmcexi  30107  lnconi  30114  lnopcnbd  30117  lnfncnbd  30138  riesz3i  30143  riesz1  30146  cnlnadjlem2  30149  cnlnadjlem8  30155  cnlnadjlem9  30156  adjbd1o  30166  branmfn  30186  opsqrlem1  30221  pjnmopi  30229  strlem1  30331  stri  30338  hstri  30346  cvcon3  30365  cvnbtwn  30367  superpos  30435  shatomici  30439  atcvat4i  30478  mdsymlem2  30485  cdj1i  30514  cdj3i  30522  rexunirn  30559  foresf1o  30569  iundisjf  30647  elunirn2  30708  aciunf1lem  30719  fnpreimac  30728  fgreu  30729  fcnvgreu  30730  xrge0infss  30803  ssnnssfz  30828  iundisjfi  30837  xreceu  30916  rexdiv  30920  isarchi3  31160  archirngz  31162  archiabllem2a  31167  rhmdvdsr  31236  0nellinds  31280  qtophaus  31500  reff  31503  locfinreflem  31504  cmpcref  31514  dispcmp  31523  metidval  31554  pstmval  31559  tpr2rico  31576  pnfneige0  31615  qqhucn  31654  rrhre  31683  indf1ofs  31706  esumcst  31743  esumpcvgval  31758  dmsigagen  31824  rossros  31860  dya2icoseg  31956  dya2iocnrect  31960  dya2iocuni  31962  eulerpartlemgvv  32055  dstfrvunirn  32153  ballotlem4  32177  ballotlemic  32185  ballotlem1c  32186  ballotlemrc  32209  signsw0g  32247  signswmnd  32248  prodfzo03  32295  tgoldbachgt  32355  loop1cycl  32812  umgr2cycllem  32815  umgr2cycl  32816  subfacp1lem3  32857  erdsze2lem2  32879  cnpconn  32905  txpconn  32907  ptpconn  32908  indispconn  32909  connpconn  32910  cvxpconn  32917  cnllysconn  32920  cvmsss2  32949  cvmcov2  32950  cvmopnlem  32953  cvmliftlem14  32972  cvmliftlem15  32973  cvmlift2lem11  32988  cvmlift2lem12  32989  cvmlift2lem13  32990  cvmlift3lem2  32995  cvmlift3lem6  32999  cvmlift3lem9  33002  mthmi  33252  onelssex  33376  eldifsucnn  33410  br8  33442  br6  33443  br4  33444  dfon2lem9  33486  ssttrcl  33514  ttrcltr  33515  frxp2  33528  frxp3  33534  poseq  33539  wzel  33555  wsuclem  33556  wsuclb  33559  naddcllem  33568  elno2  33594  sltval2  33596  noreson  33600  sltres  33602  noseponlem  33604  nolesgn2o  33611  nogesgn1o  33613  nodense  33632  nosupfv  33646  nosupres  33647  nosupbnd1lem3  33650  nosupbnd1lem5  33652  nosupbnd2lem1  33655  noinffv  33661  noinfres  33662  noinfbnd1lem3  33665  noinfbnd1lem5  33667  noinfbnd2lem1  33670  noetasuplem4  33676  noetainflem4  33680  noetalem2  33682  oldlim  33806  cofcutrtime  33830  imagesset  33992  fvtransport  34071  brcolinear  34098  brsegle  34147  seglerflx  34151  seglemin  34152  btwnsegle  34156  fvray  34180  fvline  34183  hilbert1.1  34193  elhf2  34214  0hf  34216  nn0prpwlem  34248  nn0prpw  34249  fness  34275  fneref  34276  fnessref  34283  refssfne  34284  neibastop2lem  34286  fnemeet1  34292  tailfb  34303  filnetlem4  34307  limsucncmpi  34371  taupilemrplb  35225  relowlssretop  35271  rdgellim  35284  matunitlindflem2  35511  ptrecube  35514  poimirlem4  35518  poimirlem17  35531  poimirlem20  35534  poimirlem23  35537  poimirlem24  35538  poimirlem26  35540  poimirlem27  35541  poimirlem29  35543  poimirlem32  35546  heicant  35549  mblfinlem1  35551  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  volsupnfl  35559  itg2addnclem  35565  itg2addnclem3  35567  itg2addnc  35568  ftc1anclem5  35591  unirep  35608  cover2  35609  indexa  35628  frinfm  35630  sdclem1  35638  fdc  35640  incsequz  35643  caushft  35656  istotbnd3  35666  0totbnd  35668  sstotbnd2  35669  sstotbnd  35670  sstotbnd3  35671  isbnd3  35679  ssbnd  35683  equivbnd  35685  prdsbnd  35688  prdstotbnd  35689  cntotbnd  35691  heibor1lem  35704  heiborlem1  35706  heiborlem3  35708  heiborlem6  35711  heiborlem8  35713  bfplem2  35718  rrncmslem  35727  iccbnd  35735  opidonOLD  35747  exidres  35773  isrngod  35793  isgrpda  35850  isdrngo2  35853  igenval  35956  igenidl  35958  prtlem10  36616  lshpnel2N  36736  lsmsat  36759  lssatomic  36762  lcvnbtwn  36776  lfl1  36821  eqlkr  36850  lshpkrlem1  36861  lshpkrex  36869  cvrcon3b  37028  cvrat4  37194  3dim3  37220  ps-2  37229  llni  37259  llnle  37269  lplni  37283  lplnle  37291  lplnexllnN  37315  lvoli  37326  lnatexN  37530  elpaddn0  37551  pclfinN  37651  lhprelat3N  37791  4atexlemex2  37822  4atex  37827  4atex2-0aOLDN  37829  4atex2-0cOLDN  37831  lautcvr  37843  cdleme0ex1N  37974  cdleme50rnlem  38295  cdleme50ex  38310  cdlemg1cex  38339  cdlemkid5  38686  cdlemk  38725  tendoex  38726  cdleml5N  38731  cdlemm10N  38869  dih1dimatlem0  39079  dihjat1lem  39179  dvh3dim2  39199  dvh3dim3N  39200  dochkr1  39229  dochkr1OLDN  39230  lcfrvalsnN  39292  lcfrlem27  39320  lcfrlem37  39330  lcfr  39336  mapd1o  39399  mapdpglem23  39445  hdmap11lem2  39593  rspcedvdw  39902  resubeu  40068  nacsfix  40237  mzpcompact2lem  40276  eldioph  40283  diophrw  40284  diophin  40297  rexrabdioph  40319  rexzrexnn0  40329  eldioph4b  40336  rencldnfilem  40345  irrapxlem5  40351  irrapxlem6  40352  pell1234qrdich  40386  pell14qrdich  40394  infmrgelbi  40403  pellqrex  40404  pellfundre  40406  pellfundlb  40409  rmxynorm  40443  congrep  40498  acongrep  40505  jm2.27  40533  fnwe2lem2  40579  islssfgi  40600  hbtlem2  40652  hbtlem4  40654  hbtlem5  40656  dgraaub  40676  mpaaeu  40678  aaitgo  40690  rgspnval  40696  rgspncl  40697  clsk1independent  41333  elabrexg  42262  restuni3  42340  iinssd  42353  founiiun  42388  wessf1ornlem  42395  founiiun0  42401  unirnmap  42421  dstregt0  42492  uzfissfz  42538  rpgtrecnn  42592  rexabslelem  42631  infrnmptle  42636  infxrunb3rnmpt  42641  infxrpnf  42660  supminfxr  42679  iooiinicc  42755  iooiinioc  42769  uzubioo  42780  climsuse  42824  islptre  42835  limsuppnfdlem  42917  climinf3  42932  limsupmnfuzlem  42942  limsupre3lem  42948  limsupre3uzlem  42951  0cnv  42958  liminfreuzlem  43018  cnrefiisplem  43045  icccncfext  43103  cncficcgt0  43104  dvbdfbdioo  43146  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  stoweidlem9  43225  stoweidlem14  43230  stoweidlem18  43234  stoweidlem21  43237  stoweidlem29  43245  stoweidlem34  43250  stoweidlem35  43251  stoweidlem39  43255  stoweidlem41  43257  stoweidlem45  43261  stoweidlem52  43268  stoweidlem55  43271  stoweidlem57  43273  stoweidlem60  43276  stirlinglem5  43294  stirlinglem13  43302  stirlinglem14  43303  fourierdlem16  43339  fourierdlem20  43343  fourierdlem21  43344  fourierdlem22  43345  fourierdlem25  43348  fourierdlem31  43354  fourierdlem39  43362  fourierdlem41  43364  fourierdlem42  43365  fourierdlem47  43369  fourierdlem48  43370  fourierdlem49  43371  fourierdlem51  43373  fourierdlem63  43385  fourierdlem64  43386  fourierdlem65  43387  fourierdlem77  43399  fourierdlem81  43403  fourierdlem83  43405  fourierdlem103  43425  fourierdlem104  43426  elaa2lem  43449  etransclem47  43497  qndenserrnbl  43511  ioorrnopnlem  43520  ioorrnopnxrlem  43522  intsaluni  43543  salgencntex  43557  subsaliuncllem  43571  sge0resplit  43619  sge0seq  43659  sge0reuz  43660  nnfoctbdjlem  43668  meaiininclem  43699  hoicvrrex  43769  ovnlecvr  43771  ovnlerp  43775  hoidmv1lelem2  43805  hoidmvlelem2  43809  hoidmvlelem3  43810  ovnhoilem1  43814  ovnlecvr2  43823  hoiqssbl  43838  ovolval4lem2  43863  ovolval5lem2  43866  ovnovollem1  43869  ovnovollem2  43870  iinhoiicclem  43886  smfinflem  44022  smflimsuplem7  44031  sprsymrelfolem2  44618  perfectALTV  44848  9gbo  44899  11gbo  44900  nnsum3primes4  44913  nnsum3primesprm  44915  ssnn0ssfz  45358  lincsumcl  45445  lincscmcl  45446  zlmodzxzldep  45518  ldepsnlinc  45522  line2ylem  45770  line2xlem  45772  rspceb2dv  45821  sepfsepc  45894  lubsscl  45927  glbsscl  45928  aacllem  46176