Theorem rspcev 3562

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071

This theorem is referenced by:  rspceaimv  3566  rspc2ev  3573  rspc3ev  3575  rspceeqv  3576  reu6i  3664  rspesbca  3815  eliuni  4931  iuneqconst  4936  brralrspcev  5135  wefrc  5584  wereu2  5587  xpdifid  6076  frpomin  6247  onfr  6309  ordunidif  6318  eliman0  6818  dffv2  6872  elrnrexdm  6974  eldmrexrn  6976  elabrex  7125  elunirn2  7135  f1elima  7145  fliftfun  7192  fliftval  7196  f1oiso2  7232  sorpssuni  7594  sorpssint  7595  onssmin  7651  onminex  7661  fimaproj  7985  tfrlem12  8229  seqomlem2  8291  oawordeulem  8394  oaass  8401  odi  8419  omass  8420  omeulem1  8422  oen0  8426  oelim2  8435  oeeulem  8441  nnawordex  8477  eldifsucnn  8503  boxcutc  8738  snfi  8843  rexdif1en  8953  findcard  8955  nnfi  8959  pssnn  8960  ssnnfiOLD  8962  unfi  8964  pwfir  8968  onfin  9022  pssnnOLD  9049  dif1enALT  9059  frfi  9068  fisupg  9071  nnsdomg  9082  unfiOLD  9090  fissuni  9133  fipreima  9134  finsschain  9135  indexfi  9136  marypha1lem  9201  eqsup  9224  supmax  9235  fisup2g  9236  fisupcl  9237  supisoex  9242  infmin  9262  fiinfg  9267  fiinf2g  9268  wofib  9313  wemaplem2  9315  card2inf  9323  brwdom2  9341  cnfcom3clem  9472  ssttrcl  9482  ttrcltr  9483  trcl  9495  frmin  9516  r1ordg  9545  r1pwss  9551  tz9.12lem3  9556  tz9.12  9557  r1elwf  9563  tcrank  9651  scottex  9652  scott0  9653  isnumi  9713  onsdom  9763  ondomen  9802  infpwfien  9827  cardaleph  9854  infenaleph  9856  alephfplem4  9872  alephfp2  9874  dfac2b  9895  ackbij1lem18  10002  ackbij1  10003  cflem  10011  cflecard  10018  cfsuc  10022  cfflb  10024  cofsmo  10034  coftr  10038  fin23lem7  10081  fin23lem11  10082  enfin2i  10086  fin23lem26  10090  isf32lem5  10122  isf34lem4  10142  isfin1-3  10151  fin1a2lem7  10171  axdc3lem4  10218  ttukeylem7  10280  iunfo  10304  ficard  10330  pwcfsdom  10348  fpwwe2lem11  10406  wunex  10504  eltsk2g  10516  grur1  10585  axgroth6  10593  inaprc  10601  nqereu  10694  archnq  10745  genpnmax  10772  ltexpri  10808  prlem936  10812  recexpr  10816  supexpr  10819  negexsr  10867  recexsrlem  10868  recexsr  10872  supsrlem  10876  axrnegex  10927  axrrecex  10928  axpre-sup  10934  1re  10984  dedekind  11147  dedekindle  11148  cnegex  11165  cnegex2  11166  recex  11616  receu  11629  fiminre2  11932  cju  11978  nn2ge  12009  nominpos  12219  zdiv  12399  btwnz  12432  uzwo  12660  ublbneg  12682  lbzbi  12685  zsupss  12686  uzsupss  12689  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem4  12729  rpnnen1lem5  12730  z2ge  12941  qbtwnre  12942  qbtwnxr  12943  xralrple  12948  xrsupsslem  13050  xrinfmsslem  13051  supxrpnf  13061  icc0  13136  uzsup  13592  expnbnd  13956  expmulnbnd  13959  hashkf  14055  hashdom  14103  iswrdi  14230  rtrclreclem1  14777  rtrclreclem2  14779  rtrclreclem3  14780  01sqrex  14970  resqrex  14971  sqrtneg  14988  abs1m  15056  rexanuz  15066  rexuz3  15069  rexuzre  15073  sqreu  15081  o1lo1  15255  climconst  15261  rlimclim1  15263  climshftlem  15292  rlimo1  15335  lo1add  15345  lo1mul  15346  lo1le  15372  isercoll  15388  serf0  15401  zsum  15439  fsum  15441  fsumcvg3  15450  mertenslem1  15605  ntrivcvgn0  15619  ntrivcvgmullem  15622  zprod  15656  fprod  15660  fprodntriv  15661  dvdsval2  15975  dvds0lem  15985  dvds1lem  15986  dvds2lem  15987  odd2np1lem  16058  odd2np1  16059  opeo  16083  omeo  16084  divalglem9  16119  gcdcllem3  16217  lcmcllem  16310  qredeu  16372  exprmfct  16418  isprm5  16421  odzcllem  16502  reumodprminv  16514  modprm0  16515  nnnn0modprm0  16516  pythagtriplem19  16543  pcprmpw2  16592  pockthi  16617  infpnlem2  16621  vdwlem2  16692  vdwlem10  16700  vdwlem13  16703  ramub1lem1  16736  cshwrepswhash1  16813  imasleval  17261  mreexexlem3d  17364  mreexexlem4d  17365  iscatd  17391  cat1  17821  poslubd  18140  fpwipodrs  18267  ismgmid2  18361  mgmidsssn0  18365  gsumval2a  18378  ismndd  18416  isgrpd2  18608  isgrpd  18610  imasgrp2  18699  mhmmnd  18706  ghmgrp  18708  gaorber  18923  orbsta  18928  cayleyth  19032  pmtrdifel  19097  pmtrdifwrdel  19102  pmtrdifwrdel2  19103  psgnunilem2  19112  psgnunilem3  19113  psgnvalii  19126  pgpfi1  19209  sylow1lem3  19214  sylow1lem5  19216  pgpfi  19219  sylow2alem2  19232  efgredeu  19367  lt6abl  19505  pgpfac1lem3a  19688  pgpfac1lem3  19689  pgpfac1lem5  19691  pgpfaclem1  19693  pgpfaclem3  19695  ablfaclem2  19698  dvdsrmul  19899  dvdsr01  19906  irredrmul  19958  lspf  20245  lspval  20246  lssats2  20271  lspfixed  20399  lspsolvlem  20413  zringlpir  20698  zncyg  20765  cygth  20788  frlmup4  21017  aspval  21086  evlseu  21302  fiinbas  22111  topbas  22131  pptbas  22167  clsval  22197  elcls  22233  neiint  22264  neips  22273  opnneissb  22274  opnssneib  22275  innei  22285  neiptopnei  22292  restbas  22318  neitr  22340  pnfnei  22380  mnfnei  22381  lmconst  22421  iscnp4  22423  cncnpi  22438  cnconst2  22443  cnprest  22449  cnpdis  22453  nrmsep  22517  regsep2  22536  cmpcovf  22551  cmpsub  22560  cmpcld  22562  hauscmplem  22566  conncompid  22591  2ndci  22608  2ndcsb  22609  2ndc1stc  22611  1stcrest  22613  2ndcctbss  22615  2ndcdisj  22616  2ndcomap  22618  2ndcsep  22619  dis2ndc  22620  restlly  22643  islly2  22644  hausllycmp  22654  cldllycmp  22655  lly1stc  22656  dislly  22657  ssref  22672  refref  22673  finlocfin  22680  dissnlocfin  22689  locfindis  22690  llycmpkgen2  22710  cmpkgen  22711  1stckgenlem  22713  elptr  22733  ptbasfi  22741  neitx  22767  ptpjopn  22772  txcnp  22780  ptcnplem  22781  txlly  22796  txnlly  22797  txtube  22800  txcmplem1  22801  tx1stc  22810  txkgen  22812  xkococnlem  22819  txconn  22849  tgqtop  22872  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  reghmph  22953  nrmhmph  22954  fbssfi  22997  opnfbas  23002  isfil2  23016  fsubbas  23027  ssfg  23032  fgss2  23034  fbasrn  23044  filuni  23045  fgtr  23050  ssufl  23078  uffix  23081  elfm2  23108  elfm3  23110  imaelfm  23111  rnelfmlem  23112  rnelfm  23113  fmfnfmlem4  23117  fmfnfm  23118  fmco  23121  ufldom  23122  hausflim  23141  flimcls  23145  hauspwpwf1  23147  flffbas  23155  txflf  23166  fclscf  23185  fclsfnflim  23187  alexsubALTlem4  23210  alexsubALT  23211  tmdgsum2  23256  symgtgp  23266  subgntr  23267  opnsubg  23268  ghmcnp  23275  qustgpopn  23280  tsmsfbas  23288  tsmsxplem1  23313  ustexsym  23376  elrnust  23385  trust  23390  utoptop  23395  restutop  23398  restutopopn  23399  ustuqtop4  23405  utopsnneiplem  23408  iducn  23444  fmucnd  23453  cfilufg  23454  trcfilu  23455  neipcfilu  23457  imasdsf1olem  23535  blssps  23586  blss  23587  blssexps  23588  blssex  23589  ssblex  23590  blin2  23591  neibl  23666  blcld  23670  metss2  23677  stdbdmopn  23683  met1stc  23686  met2ndci  23687  metrest  23689  prdsxmslem2  23694  metcnp3  23705  metuval  23714  metustexhalf  23721  metustfbas  23722  cfilucfil  23724  restmetu  23735  dscopn  23738  ngptgp  23801  nlmvscnlem1  23859  tgioo  23968  tgqioo  23972  xrsmopn  23984  zcld  23985  recld2  23986  zdis  23988  icccmplem1  23994  icccmplem2  23995  xmetdcn2  24009  addcnlem  24036  xrhmeo  24118  cnheibor  24127  cnllycmp  24128  lebnumlem3  24135  lebnum  24136  xlebnum  24137  lebnumii  24138  elpi1i  24218  ipcnlem1  24418  lmnn  24436  iscfil3  24446  cfilres  24469  flimcfil  24487  bcthlem4  24500  bcthlem5  24501  minveclem4c  24598  minveclem2  24599  minveclem3b  24601  minveclem3  24602  minveclem4  24605  minveclem6  24607  ivthlem2  24625  ivth  24627  ivthle  24629  ivthle2  24630  elovolmr  24649  ovolunlem1  24670  ovoliunlem2  24676  ovolicc1  24689  iundisj  24721  iunmbl2  24730  dyadmbllem  24772  volivth  24780  mbflimsup  24839  i1faddlem  24866  i1fmullem  24867  itg2lr  24904  itg2monolem1  24924  limcnlp  25051  ellimc3  25052  limcflf  25054  limciun  25067  rollelem  25162  c1lip1  25170  lhop1lem  25186  ply1divex  25310  ig1peu  25345  elply2  25366  coeeq  25397  plydivlem3  25464  plydivlem4  25465  elqaalem3  25490  qaa  25492  iaa  25494  aareccl  25495  aannenlem2  25498  aalioulem2  25502  aalioulem3  25503  aalioulem5  25505  aalioulem6  25506  aaliou  25507  aaliou2  25509  aaliou3lem8  25514  ulmshftlem  25557  reeff1o  25615  pilem2  25620  pilem3  25621  efif1olem2  25708  efopn  25822  cxpcn3lem  25909  cxpeq  25919  dcubic2  26003  quart  26020  xrlimcnp  26127  ftalem5  26235  ftalem7  26237  sgmnncl  26305  dvdsppwf1o  26344  musum  26349  perfect  26388  dchrptlem1  26421  dchrptlem2  26422  dchrpt  26424  bpos1lem  26439  lgsqrlem4  26506  lgsdchrval  26511  2sqblem  26588  dchrisumlem3  26648  chpdifbndlem2  26711  pntrsumbnd2  26724  pntpbnd1  26743  pntpbnd2  26744  pntpbnd  26745  pntibndlem2  26748  pntibndlem3  26749  pntleme  26765  pntlem3  26766  axtgcont  26839  tgcgrxfr  26888  legid  26957  btwnleg  26958  leg0  26962  tghilberti1  27007  tglnpt2  27011  colline  27019  mirreu3  27024  isperp2  27085  colperpex  27103  lnopp2hpgb  27133  hpgerlem  27135  brbtwn  27276  brcgr  27277  brbtwn2  27282  axpasch  27318  axlowdimlem14  27332  axlowdim2  27337  axcontlem2  27342  axcontlem4  27344  axcontlem8  27348  axcontlem10  27350  axcontlem12  27352  fusgrn0degnn0  27875  friendshipgt3  28771  lpni  28851  isgrpoi  28869  vacn  29065  smcnlem  29068  nmosetn0  29136  nmoolb  29142  nmobndi  29146  nmoo0  29162  nmlno0lem  29164  isblo3i  29172  blo3i  29173  blocnilem  29175  ubthlem1  29241  minvecolem2  29246  minvecolem3  29247  minvecolem4c  29250  minvecolem4  29251  minvecolem5  29252  minvecolem6  29253  norm1exi  29621  occl  29675  spanval  29704  spancl  29707  shsval2i  29758  ococin  29779  pjoml6i  29960  nmopsetn0  30236  nmfnsetn0  30249  nmoplb  30278  nmfnlb  30295  nmop0  30357  nmfn0  30358  nmlnop0iALT  30366  nmopun  30385  nmcexi  30397  lnconi  30404  lnopcnbd  30407  lnfncnbd  30428  riesz3i  30433  riesz1  30436  cnlnadjlem2  30439  cnlnadjlem8  30445  cnlnadjlem9  30446  adjbd1o  30456  branmfn  30476  opsqrlem1  30511  pjnmopi  30519  strlem1  30621  stri  30628  hstri  30636  cvcon3  30655  cvnbtwn  30657  superpos  30725  shatomici  30729  atcvat4i  30768  mdsymlem2  30775  cdj1i  30804  cdj3i  30812  rexunirn  30849  foresf1o  30859  iundisjf  30937  aciunf1lem  31008  fnpreimac  31017  fgreu  31018  fcnvgreu  31019  xrge0infss  31092  ssnnssfz  31117  iundisjfi  31126  xreceu  31205  rexdiv  31209  isarchi3  31450  archirngz  31452  archiabllem2a  31457  rhmdvdsr  31526  0nellinds  31575  qtophaus  31795  reff  31798  locfinreflem  31799  cmpcref  31809  dispcmp  31818  metidval  31849  pstmval  31854  tpr2rico  31871  pnfneige0  31910  qqhucn  31951  rrhre  31980  indf1ofs  32003  esumcst  32040  esumpcvgval  32055  dmsigagen  32121  rossros  32157  dya2icoseg  32253  dya2iocnrect  32257  dya2iocuni  32259  eulerpartlemgvv  32352  dstfrvunirn  32450  ballotlem4  32474  ballotlemic  32482  ballotlem1c  32483  ballotlemrc  32506  signsw0g  32544  signswmnd  32545  prodfzo03  32592  tgoldbachgt  32652  loop1cycl  33108  umgr2cycllem  33111  umgr2cycl  33112  subfacp1lem3  33153  erdsze2lem2  33175  cnpconn  33201  txpconn  33203  ptpconn  33204  indispconn  33205  connpconn  33206  cvxpconn  33213  cnllysconn  33216  cvmsss2  33245  cvmcov2  33246  cvmopnlem  33249  cvmliftlem14  33268  cvmliftlem15  33269  cvmlift2lem11  33284  cvmlift2lem12  33285  cvmlift2lem13  33286  cvmlift3lem2  33291  cvmlift3lem6  33295  cvmlift3lem9  33298  mthmi  33548  onelssex  33670  br8  33732  br6  33733  br4  33734  dfon2lem9  33776  frxp2  33800  frxp3  33806  poseq  33811  wzel  33827  wsuclem  33828  wsuclb  33831  naddcllem  33840  elno2  33866  sltval2  33868  noreson  33872  sltres  33874  noseponlem  33876  nolesgn2o  33883  nogesgn1o  33885  nodense  33904  nosupfv  33918  nosupres  33919  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd2lem1  33927  noinffv  33933  noinfres  33934  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noinfbnd2lem1  33942  noetasuplem4  33948  noetainflem4  33952  noetalem2  33954  oldlim  34078  cofcutrtime  34102  imagesset  34264  fvtransport  34343  brcolinear  34370  brsegle  34419  seglerflx  34423  seglemin  34424  btwnsegle  34428  fvray  34452  fvline  34455  hilbert1.1  34465  elhf2  34486  0hf  34488  nn0prpwlem  34520  nn0prpw  34521  fness  34547  fneref  34548  fnessref  34555  refssfne  34556  neibastop2lem  34558  fnemeet1  34564  tailfb  34575  filnetlem4  34579  limsucncmpi  34643  taupilemrplb  35500  relowlssretop  35543  rdgellim  35556  matunitlindflem2  35783  ptrecube  35786  poimirlem4  35790  poimirlem17  35803  poimirlem20  35806  poimirlem23  35809  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem32  35818  heicant  35821  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  volsupnfl  35831  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  ftc1anclem5  35863  unirep  35880  cover2  35881  indexa  35900  frinfm  35902  sdclem1  35910  fdc  35912  incsequz  35915  caushft  35928  istotbnd3  35938  0totbnd  35940  sstotbnd2  35941  sstotbnd  35942  sstotbnd3  35943  isbnd3  35951  ssbnd  35955  equivbnd  35957  prdsbnd  35960  prdstotbnd  35961  cntotbnd  35963  heibor1lem  35976  heiborlem1  35978  heiborlem3  35980  heiborlem6  35983  heiborlem8  35985  bfplem2  35990  rrncmslem  35999  iccbnd  36007  opidonOLD  36019  exidres  36045  isrngod  36065  isgrpda  36122  isdrngo2  36125  igenval  36228  igenidl  36230  prtlem10  36886  lshpnel2N  37006  lsmsat  37029  lssatomic  37032  lcvnbtwn  37046  lfl1  37091  eqlkr  37120  lshpkrlem1  37131  lshpkrex  37139  cvrcon3b  37298  cvrat4  37464  3dim3  37490  ps-2  37499  llni  37529  llnle  37539  lplni  37553  lplnle  37561  lplnexllnN  37585  lvoli  37596  lnatexN  37800  elpaddn0  37821  pclfinN  37921  lhprelat3N  38061  4atexlemex2  38092  4atex  38097  4atex2-0aOLDN  38099  4atex2-0cOLDN  38101  lautcvr  38113  cdleme0ex1N  38244  cdleme50rnlem  38565  cdleme50ex  38580  cdlemg1cex  38609  cdlemkid5  38956  cdlemk  38995  tendoex  38996  cdleml5N  39001  cdlemm10N  39139  dih1dimatlem0  39349  dihjat1lem  39449  dvh3dim2  39469  dvh3dim3N  39470  dochkr1  39499  dochkr1OLDN  39500  lcfrvalsnN  39562  lcfrlem27  39590  lcfrlem37  39600  lcfr  39606  mapd1o  39669  mapdpglem23  39715  hdmap11lem2  39863  rspcedvdw  40186  resubeu  40367  nacsfix  40541  mzpcompact2lem  40580  eldioph  40587  diophrw  40588  diophin  40601  rexrabdioph  40623  rexzrexnn0  40633  eldioph4b  40640  rencldnfilem  40649  irrapxlem5  40655  irrapxlem6  40656  pell1234qrdich  40690  pell14qrdich  40698  infmrgelbi  40707  pellqrex  40708  pellfundre  40710  pellfundlb  40713  rmxynorm  40747  congrep  40802  acongrep  40809  jm2.27  40837  fnwe2lem2  40883  islssfgi  40904  hbtlem2  40956  hbtlem4  40958  hbtlem5  40960  dgraaub  40980  mpaaeu  40982  aaitgo  40994  rgspnval  41000  rgspncl  41001  sucomisnotcard  41158  clsk1independent  41663  elabrexg  42596  restuni3  42674  iinssd  42687  founiiun  42722  wessf1ornlem  42729  founiiun0  42735  unirnmap  42755  dstregt0  42827  uzfissfz  42872  rpgtrecnn  42926  rexabslelem  42965  infrnmptle  42970  infxrunb3rnmpt  42975  infxrpnf  42993  supminfxr  43011  iooiinicc  43087  iooiinioc  43101  uzubioo  43112  climsuse  43156  islptre  43167  limsuppnfdlem  43249  climinf3  43264  limsupmnfuzlem  43274  limsupre3lem  43280  limsupre3uzlem  43283  0cnv  43290  liminfreuzlem  43350  cnrefiisplem  43377  icccncfext  43435  cncficcgt0  43436  dvbdfbdioo  43478  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem9  43557  stoweidlem14  43562  stoweidlem18  43566  stoweidlem21  43569  stoweidlem29  43577  stoweidlem34  43582  stoweidlem35  43583  stoweidlem39  43587  stoweidlem41  43589  stoweidlem45  43593  stoweidlem52  43600  stoweidlem55  43603  stoweidlem57  43605  stoweidlem60  43608  stirlinglem5  43626  stirlinglem13  43634  stirlinglem14  43635  fourierdlem16  43671  fourierdlem20  43675  fourierdlem21  43676  fourierdlem22  43677  fourierdlem25  43680  fourierdlem31  43686  fourierdlem39  43694  fourierdlem41  43696  fourierdlem42  43697  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem51  43705  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem77  43731  fourierdlem81  43735  fourierdlem83  43737  fourierdlem103  43757  fourierdlem104  43758  elaa2lem  43781  etransclem47  43829  qndenserrnbl  43843  ioorrnopnlem  43852  ioorrnopnxrlem  43854  intsaluni  43875  salgencntex  43889  subsaliuncllem  43903  sge0resplit  43951  sge0seq  43991  sge0reuz  43992  nnfoctbdjlem  44000  meaiininclem  44031  hoicvrrex  44101  ovnlecvr  44103  ovnlerp  44107  hoidmv1lelem2  44137  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  ovnlecvr2  44155  hoiqssbl  44170  ovolval4lem2  44195  ovolval5lem2  44198  ovnovollem1  44201  ovnovollem2  44202  iinhoiicclem  44218  smfinflem  44361  smflimsuplem7  44370  sprsymrelfolem2  44956  perfectALTV  45186  9gbo  45237  11gbo  45238  nnsum3primes4  45251  nnsum3primesprm  45253  ssnn0ssfz  45696  lincsumcl  45783  lincscmcl  45784  zlmodzxzldep  45856  ldepsnlinc  45860  line2ylem  46108  line2xlem  46110  rspceb2dv  46159  sepfsepc  46232  lubsscl  46265  glbsscl  46266  aacllem  46516