Theorem rspcev 3621

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2138, ax-11 2154, ax-12 2174. (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 3614	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068

This theorem is referenced by:  rspcedvdw  3624  rspceb2dv  3625  rspceaimv  3627  rspc2ev  3634  rspc3ev  3638  rspceeqv  3644  reu6i  3736  rspesbca  3889  eliuni  5001  iuneqconst  5007  brralrspcev  5207  wefrc  5682  wereu2  5685  xpdifid  6189  frpomin  6362  onfr  6424  onelssex  6433  ordunidif  6434  eliman0  6946  dffv2  7003  elrnrexdm  7108  eldmrexrn  7110  elabrex  7261  elabrexg  7262  elunirn2OLD  7272  f1elima  7282  fliftfun  7331  fliftval  7335  f1oiso2  7371  sorpssuni  7750  sorpssint  7751  onssmin  7811  onminex  7821  fimaproj  8158  frxp3  8174  poseq  8181  tfrlem12  8427  seqomlem2  8489  oawordeulem  8590  oaass  8597  odi  8615  omass  8616  omeulem1  8618  oen0  8622  oelim2  8631  oeeulem  8637  nnawordex  8673  nnaordex2  8675  eldifsucnn  8700  cofon1  8708  cofon2  8709  naddcllem  8712  naddunif  8729  boxcutc  8979  0fi  9080  snfi  9081  snfiOLD  9082  rexdif1en  9196  rexdif1enOLD  9197  findcard  9201  nnfi  9205  pssnn  9206  unfi  9209  onfin  9264  dif1ennnALT  9308  frfi  9318  fisupg  9321  nnsdomg  9332  nnsdomgOLD  9333  pwfir  9352  prfi  9360  fissuni  9394  fipreima  9395  finsschain  9396  indexfi  9397  marypha1lem  9470  eqsup  9493  supmax  9504  fisup2g  9505  fisupcl  9506  supisoex  9511  infmin  9531  fiinfg  9536  fiinf2g  9537  wofib  9582  wemaplem2  9584  card2inf  9592  brwdom2  9610  cnfcom3clem  9742  ssttrcl  9752  ttrcltr  9753  trcl  9765  frmin  9786  r1ordg  9815  r1pwss  9821  tz9.12lem3  9826  tz9.12  9827  r1elwf  9833  tcrank  9921  scottex  9922  scott0  9923  isnumi  9983  onsdom  10033  ondomen  10074  infpwfien  10099  cardaleph  10126  infenaleph  10128  alephfplem4  10144  alephfp2  10146  dfac2b  10168  ackbij1lem18  10273  ackbij1  10274  cflem  10282  cflemOLD  10283  cflecard  10290  cfsuc  10294  cfflb  10296  cofsmo  10306  coftr  10310  fin23lem7  10353  fin23lem11  10354  enfin2i  10358  fin23lem26  10362  isf32lem5  10394  isf34lem4  10414  isfin1-3  10423  fin1a2lem7  10443  axdc3lem4  10490  ttukeylem7  10552  iunfo  10576  ficard  10602  pwcfsdom  10620  fpwwe2lem11  10678  wunex  10776  eltsk2g  10788  grur1  10857  axgroth6  10865  inaprc  10873  nqereu  10966  archnq  11017  genpnmax  11044  ltexpri  11080  prlem936  11084  recexpr  11088  supexpr  11091  negexsr  11139  recexsrlem  11140  recexsr  11144  supsrlem  11148  axrnegex  11199  axrrecex  11200  axpre-sup  11206  1re  11258  dedekind  11421  dedekindle  11422  cnegex  11439  cnegex2  11440  recex  11892  receu  11905  fiminre2  12213  cju  12259  nn2ge  12290  nominpos  12500  zdiv  12685  btwnz  12718  uzwo  12950  ublbneg  12972  lbzbi  12975  zsupss  12976  uzsupss  12979  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem4  13019  rpnnen1lem5  13020  z2ge  13236  qbtwnre  13237  qbtwnxr  13238  xralrple  13243  xrsupsslem  13345  xrinfmsslem  13346  supxrpnf  13356  icc0  13431  uzsup  13899  expnbnd  14267  expmulnbnd  14270  hashkf  14367  hashdom  14414  iswrdi  14552  rtrclreclem1  15092  rtrclreclem2  15094  rtrclreclem3  15095  01sqrex  15284  resqrex  15285  sqrtneg  15302  abs1m  15370  rexanuz  15380  rexuz3  15383  rexuzre  15387  sqreu  15395  o1lo1  15569  climconst  15575  rlimclim1  15577  climshftlem  15606  rlimo1  15649  lo1add  15659  lo1mul  15660  lo1le  15684  isercoll  15700  serf0  15713  zsum  15750  fsum  15752  fsumcvg3  15761  mertenslem1  15916  ntrivcvgn0  15930  ntrivcvgmullem  15933  zprod  15969  fprod  15973  fprodntriv  15974  dvdsval2  16289  dvds0lem  16300  dvds1lem  16301  dvds2lem  16302  odd2np1lem  16373  odd2np1  16374  opeo  16398  omeo  16399  divalglem9  16434  gcdcllem3  16534  lcmcllem  16629  qredeu  16691  exprmfct  16737  isprm5  16740  odzcllem  16825  reumodprminv  16837  modprm0  16838  nnnn0modprm0  16839  pythagtriplem19  16866  pcprmpw2  16915  pockthi  16940  infpnlem2  16944  vdwlem2  17015  vdwlem10  17023  vdwlem13  17026  ramub1lem1  17059  cshwrepswhash1  17136  imasleval  17587  mreexexlem3d  17690  mreexexlem4d  17691  iscatd  17717  cat1  18150  poslubd  18470  fpwipodrs  18597  ismgmid2  18693  mgmidsssn0  18697  gsumval2a  18710  ismndd  18781  isgrpd2  18986  isgrpd  18988  imasgrp2  19085  mhmmnd  19094  ghmgrp  19096  gaorber  19338  orbsta  19343  cayleyth  19447  pmtrdifel  19512  pmtrdifwrdel  19517  pmtrdifwrdel2  19518  psgnunilem2  19527  psgnunilem3  19528  psgnvalii  19541  pgpfi1  19627  sylow1lem3  19632  sylow1lem5  19634  pgpfi  19637  sylow2alem2  19650  efgredeu  19784  lt6abl  19927  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfac1lem5  20113  pgpfaclem1  20115  pgpfaclem3  20117  ablfaclem2  20120  dvdsrmul  20380  dvdsr01  20387  irredrmul  20443  rhmdvdsr  20524  rgspnval  20628  rgspncl  20629  lspf  20989  lspval  20990  lssats2  21015  lspfixed  21147  lspsolvlem  21161  zringlpir  21495  pzriprnglem13  21521  zncyg  21584  cygth  21607  frlmup4  21838  aspval  21910  evlseu  22124  fiinbas  22974  topbas  22994  pptbas  23030  clsval  23060  elcls  23096  neiint  23127  neips  23136  opnneissb  23137  opnssneib  23138  innei  23148  neiptopnei  23155  restbas  23181  neitr  23203  pnfnei  23243  mnfnei  23244  lmconst  23284  iscnp4  23286  cncnpi  23301  cnconst2  23306  cnprest  23312  cnpdis  23316  nrmsep  23380  regsep2  23399  cmpcovf  23414  cmpsub  23423  cmpcld  23425  hauscmplem  23429  conncompid  23454  2ndci  23471  2ndcsb  23472  2ndc1stc  23474  1stcrest  23476  2ndcctbss  23478  2ndcdisj  23479  2ndcomap  23481  2ndcsep  23482  dis2ndc  23483  restlly  23506  islly2  23507  hausllycmp  23517  cldllycmp  23518  lly1stc  23519  dislly  23520  ssref  23535  refref  23536  finlocfin  23543  dissnlocfin  23552  locfindis  23553  llycmpkgen2  23573  cmpkgen  23574  1stckgenlem  23576  elptr  23596  ptbasfi  23604  neitx  23630  ptpjopn  23635  txcnp  23643  ptcnplem  23644  txlly  23659  txnlly  23660  txtube  23663  txcmplem1  23664  tx1stc  23673  txkgen  23675  xkococnlem  23682  txconn  23712  tgqtop  23735  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  reghmph  23816  nrmhmph  23817  fbssfi  23860  opnfbas  23865  isfil2  23879  fsubbas  23890  ssfg  23895  fgss2  23897  fbasrn  23907  filuni  23908  fgtr  23913  ssufl  23941  uffix  23944  elfm2  23971  elfm3  23973  imaelfm  23974  rnelfmlem  23975  rnelfm  23976  fmfnfmlem4  23980  fmfnfm  23981  fmco  23984  ufldom  23985  hausflim  24004  flimcls  24008  hauspwpwf1  24010  flffbas  24018  txflf  24029  fclscf  24048  fclsfnflim  24050  alexsubALTlem4  24073  alexsubALT  24074  tmdgsum2  24119  symgtgp  24129  subgntr  24130  opnsubg  24131  ghmcnp  24138  qustgpopn  24143  tsmsfbas  24151  tsmsxplem1  24176  ustexsym  24239  trust  24253  utoptop  24258  restutop  24261  restutopopn  24262  ustuqtop4  24268  utopsnneiplem  24271  iducn  24307  fmucnd  24316  cfilufg  24317  trcfilu  24318  neipcfilu  24320  imasdsf1olem  24398  blssps  24449  blss  24450  blssexps  24451  blssex  24452  ssblex  24453  blin2  24454  neibl  24529  blcld  24533  metss2  24540  stdbdmopn  24546  met1stc  24549  met2ndci  24550  metrest  24552  prdsxmslem2  24557  metcnp3  24568  metustexhalf  24584  metustfbas  24585  cfilucfil  24587  restmetu  24598  dscopn  24601  ngptgp  24664  nlmvscnlem1  24722  tgioo  24831  tgqioo  24835  xrsmopn  24847  zcld  24848  recld2  24849  zdis  24851  icccmplem1  24857  icccmplem2  24858  xmetdcn2  24872  addcnlem  24899  xrhmeo  24990  cnheibor  25000  cnllycmp  25001  lebnumlem3  25008  lebnum  25009  xlebnum  25010  lebnumii  25011  elpi1i  25092  ipcnlem1  25292  lmnn  25310  iscfil3  25320  cfilres  25343  flimcfil  25361  bcthlem4  25374  bcthlem5  25375  minveclem4c  25472  minveclem2  25473  minveclem3b  25475  minveclem3  25476  minveclem4  25479  minveclem6  25481  ivthlem2  25500  ivth  25502  ivthle  25504  ivthle2  25505  elovolmr  25524  ovolunlem1  25545  ovoliunlem2  25551  ovolicc1  25564  iundisj  25596  iunmbl2  25605  dyadmbllem  25647  volivth  25655  mbflimsup  25714  i1faddlem  25741  i1fmullem  25742  itg2lr  25779  itg2monolem1  25799  limcnlp  25927  ellimc3  25928  limcflf  25930  limciun  25943  rollelem  26041  c1lip1  26050  lhop1lem  26066  ply1divex  26190  ig1peu  26228  elply2  26249  coeeq  26280  plydivlem3  26351  plydivlem4  26352  elqaalem3  26377  qaa  26379  iaa  26381  aareccl  26382  aannenlem2  26385  aalioulem2  26389  aalioulem3  26390  aalioulem5  26392  aalioulem6  26393  aaliou  26394  aaliou2  26396  aaliou3lem8  26401  ulmshftlem  26446  reeff1o  26505  pilem2  26510  pilem3  26511  efif1olem2  26599  efopn  26714  cxpcn3lem  26804  cxpeq  26814  dcubic2  26901  quart  26918  xrlimcnp  27025  ftalem5  27134  ftalem7  27136  sgmnncl  27204  dvdsppwf1o  27243  musum  27248  perfect  27289  dchrptlem1  27322  dchrptlem2  27323  dchrpt  27325  bpos1lem  27340  lgsqrlem4  27407  lgsdchrval  27412  2sqblem  27489  dchrisumlem3  27549  chpdifbndlem2  27612  pntrsumbnd2  27625  pntpbnd1  27644  pntpbnd2  27645  pntpbnd  27646  pntibndlem2  27649  pntibndlem3  27650  pntleme  27666  pntlem3  27667  elno2  27713  sltval2  27715  noreson  27719  sltres  27721  noseponlem  27723  nolesgn2o  27730  nogesgn1o  27732  nodense  27751  nosupfv  27765  nosupres  27766  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinffv  27780  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  noetalem2  27801  cuteq0  27891  cuteq1  27892  oldlim  27939  cofcutrtime  27975  cofss  27978  coiniss  27979  cutlt  27980  cutmax  27982  cutmin  27983  negsex  28089  negsfo  28099  norecdiv  28230  divs1  28243  precsexlem11  28255  precsex  28256  recsex  28257  elons2d  28296  n0ons  28353  dfnns2  28376  nohalf  28421  0reno  28443  readdscl  28445  axtgcont  28491  tgcgrxfr  28540  legid  28609  btwnleg  28610  leg0  28614  tghilberti1  28659  tglnpt2  28663  colline  28671  mirreu3  28676  isperp2  28737  colperpex  28755  lnopp2hpgb  28785  hpgerlem  28787  brbtwn  28928  brcgr  28929  brbtwn2  28934  axpasch  28970  axlowdimlem14  28984  axlowdim2  28989  axcontlem2  28994  axcontlem4  28996  axcontlem8  29000  axcontlem10  29002  axcontlem12  29004  fusgrn0degnn0  29531  friendshipgt3  30426  lpni  30508  isgrpoi  30526  vacn  30722  smcnlem  30725  nmosetn0  30793  nmoolb  30799  nmobndi  30803  nmoo0  30819  nmlno0lem  30821  isblo3i  30829  blo3i  30830  blocnilem  30832  ubthlem1  30898  minvecolem2  30903  minvecolem3  30904  minvecolem4c  30907  minvecolem4  30908  minvecolem5  30909  minvecolem6  30910  norm1exi  31278  occl  31332  spanval  31361  spancl  31364  shsval2i  31415  ococin  31436  pjoml6i  31617  nmopsetn0  31893  nmfnsetn0  31906  nmoplb  31935  nmfnlb  31952  nmop0  32014  nmfn0  32015  nmlnop0iALT  32023  nmopun  32042  nmcexi  32054  lnconi  32061  lnopcnbd  32064  lnfncnbd  32085  riesz3i  32090  riesz1  32093  cnlnadjlem2  32096  cnlnadjlem8  32102  cnlnadjlem9  32103  adjbd1o  32113  branmfn  32133  opsqrlem1  32168  pjnmopi  32176  strlem1  32278  stri  32285  hstri  32293  cvcon3  32312  cvnbtwn  32314  superpos  32382  shatomici  32386  atcvat4i  32425  mdsymlem2  32432  cdj1i  32461  cdj3i  32469  rexunirn  32519  foresf1o  32531  iundisjf  32608  aciunf1lem  32678  fnpreimac  32687  fgreu  32688  fcnvgreu  32689  xrge0infss  32770  ssnnssfz  32795  iundisjfi  32803  xreceu  32888  rexdiv  32892  isarchi3  33176  archirngz  33178  archiabllem2a  33183  0nellinds  33377  qtophaus  33796  reff  33799  locfinreflem  33800  cmpcref  33810  dispcmp  33819  tpr2rico  33872  pnfneige0  33911  qqhucn  33954  rrhre  33983  indf1ofs  34006  esumcst  34043  esumpcvgval  34058  dmsigagen  34124  rossros  34160  dya2icoseg  34258  dya2iocnrect  34262  dya2iocuni  34264  eulerpartlemgvv  34357  dstfrvunirn  34455  ballotlem4  34479  ballotlemic  34487  ballotlem1c  34488  ballotlemrc  34511  signsw0g  34549  signswmnd  34550  prodfzo03  34596  tgoldbachgt  34656  loop1cycl  35121  umgr2cycllem  35124  umgr2cycl  35125  subfacp1lem3  35166  erdsze2lem2  35188  cnpconn  35214  txpconn  35216  ptpconn  35217  indispconn  35218  connpconn  35219  cvxpconn  35226  cnllysconn  35229  cvmsss2  35258  cvmcov2  35259  cvmopnlem  35262  cvmliftlem14  35281  cvmliftlem15  35282  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmlift2lem13  35299  cvmlift3lem2  35304  cvmlift3lem6  35308  cvmlift3lem9  35311  mthmi  35561  r1peuqusdeg1  35627  br8  35735  br6  35736  br4  35737  dfon2lem9  35772  wzel  35805  wsuclem  35806  wsuclb  35809  imagesset  35934  fvtransport  36013  brcolinear  36040  brsegle  36089  seglerflx  36093  seglemin  36094  btwnsegle  36098  fvray  36122  fvline  36125  hilbert1.1  36135  elhf2  36156  0hf  36158  nn0prpwlem  36304  nn0prpw  36305  fness  36331  fneref  36332  fnessref  36339  refssfne  36340  neibastop2lem  36342  fnemeet1  36348  tailfb  36359  filnetlem4  36363  limsucncmpi  36427  taupilemrplb  37302  relowlssretop  37345  rdgellim  37358  matunitlindflem2  37603  ptrecube  37606  poimirlem4  37610  poimirlem17  37623  poimirlem20  37626  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem32  37638  heicant  37641  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  volsupnfl  37651  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  ftc1anclem5  37683  unirep  37700  cover2  37701  indexa  37719  frinfm  37721  sdclem1  37729  fdc  37731  incsequz  37734  caushft  37747  istotbnd3  37757  0totbnd  37759  sstotbnd2  37760  sstotbnd  37761  sstotbnd3  37762  isbnd3  37770  ssbnd  37774  equivbnd  37776  prdsbnd  37779  prdstotbnd  37780  cntotbnd  37782  heibor1lem  37795  heiborlem1  37797  heiborlem3  37799  heiborlem6  37802  heiborlem8  37804  bfplem2  37809  rrncmslem  37818  iccbnd  37826  opidonOLD  37838  exidres  37864  isrngod  37884  isgrpda  37941  isdrngo2  37944  igenval  38047  igenidl  38049  prtlem10  38846  lshpnel2N  38966  lsmsat  38989  lssatomic  38992  lcvnbtwn  39006  lfl1  39051  eqlkr  39080  lshpkrlem1  39091  lshpkrex  39099  cvrcon3b  39258  cvrat4  39425  3dim3  39451  ps-2  39460  llni  39490  llnle  39500  lplni  39514  lplnle  39522  lplnexllnN  39546  lvoli  39557  lnatexN  39761  elpaddn0  39782  pclfinN  39882  lhprelat3N  40022  4atexlemex2  40053  4atex  40058  4atex2-0aOLDN  40060  4atex2-0cOLDN  40062  lautcvr  40074  cdleme0ex1N  40205  cdleme50rnlem  40526  cdleme50ex  40541  cdlemg1cex  40570  cdlemkid5  40917  cdlemk  40956  tendoex  40957  cdleml5N  40962  cdlemm10N  41100  dih1dimatlem0  41310  dihjat1lem  41410  dvh3dim2  41430  dvh3dim3N  41431  dochkr1  41460  dochkr1OLDN  41461  lcfrvalsnN  41523  lcfrlem27  41551  lcfrlem37  41561  lcfr  41567  mapd1o  41630  mapdpglem23  41676  hdmap11lem2  41824  primrootsunit1  42078  zdivgd  42350  resubeu  42383  fidomncyc  42521  nacsfix  42699  mzpcompact2lem  42738  eldioph  42745  diophrw  42746  diophin  42759  rexrabdioph  42781  rexzrexnn0  42791  eldioph4b  42798  rencldnfilem  42807  irrapxlem5  42813  irrapxlem6  42814  pell1234qrdich  42848  pell14qrdich  42856  infmrgelbi  42865  pellqrex  42866  pellfundre  42868  pellfundlb  42871  rmxynorm  42906  congrep  42961  acongrep  42968  jm2.27  42996  fnwe2lem2  43039  islssfgi  43060  hbtlem2  43112  hbtlem4  43114  hbtlem5  43116  dgraaub  43136  mpaaeu  43138  aaitgo  43150  unielss  43206  onexgt  43228  onexomgt  43229  onexlimgt  43231  onexoegt  43232  oaordnr  43285  omnord1  43294  oenord1  43305  oaomoencom  43306  oenass  43308  tfsconcatfv2  43329  tfsconcatrn  43331  tfsconcatb0  43333  ofoafo  43345  naddcnffo  43353  oaun3lem1  43363  naddwordnexlem4  43390  sucomisnotcard  43533  clsk1independent  44035  prclaxpr  44947  restuni3  45057  iinssd  45070  founiiun  45121  wessf1ornlem  45127  founiiun0  45132  unirnmap  45150  dstregt0  45231  uzfissfz  45275  rpgtrecnn  45329  rexabslelem  45367  infrnmptle  45372  infxrunb3rnmpt  45377  infxrpnf  45395  supminfxr  45413  rexanuz2nf  45442  iooiinicc  45494  iooiinioc  45508  uzubioo  45519  climsuse  45563  islptre  45574  limsuppnfdlem  45656  climinf3  45671  limsupmnfuzlem  45681  limsupre3lem  45687  limsupre3uzlem  45690  0cnv  45697  liminfreuzlem  45757  cnrefiisplem  45784  icccncfext  45842  cncficcgt0  45843  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem9  45964  stoweidlem14  45969  stoweidlem18  45973  stoweidlem21  45976  stoweidlem29  45984  stoweidlem34  45989  stoweidlem35  45990  stoweidlem39  45994  stoweidlem41  45996  stoweidlem45  46000  stoweidlem52  46007  stoweidlem55  46010  stoweidlem57  46012  stoweidlem60  46015  stirlinglem5  46033  stirlinglem13  46041  stirlinglem14  46042  fourierdlem16  46078  fourierdlem20  46082  fourierdlem21  46083  fourierdlem22  46084  fourierdlem25  46087  fourierdlem31  46093  fourierdlem39  46101  fourierdlem41  46103  fourierdlem42  46104  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem77  46138  fourierdlem81  46142  fourierdlem83  46144  fourierdlem103  46164  fourierdlem104  46165  elaa2lem  46188  etransclem47  46236  qndenserrnbl  46250  ioorrnopnlem  46259  ioorrnopnxrlem  46261  intsaluni  46284  salgencntex  46298  subsaliuncllem  46312  sge0resplit  46361  sge0seq  46401  sge0reuz  46402  nnfoctbdjlem  46410  meaiininclem  46441  hoicvrrex  46511  ovnlecvr  46513  ovnlerp  46517  hoidmv1lelem2  46547  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  ovnlecvr2  46565  hoiqssbl  46580  ovolval4lem2  46605  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  iinhoiicclem  46628  smfinflem  46772  smflimsuplem7  46781  sprsymrelfolem2  47417  perfectALTV  47647  9gbo  47698  11gbo  47699  nnsum3primes4  47712  nnsum3primesprm  47714  ssnn0ssfz  48193  lincsumcl  48276  lincscmcl  48277  zlmodzxzldep  48349  ldepsnlinc  48353  line2ylem  48600  line2xlem  48602  sepfsepc  48723  lubsscl  48756  glbsscl  48757  aacllem  49031