Theorem rspcev 3591

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055

This theorem is referenced by:  rspcedvdw  3594  rspceb2dv  3595  rspceaimv  3597  rspc2ev  3604  rspc3ev  3608  rspceeqv  3614  reu6i  3702  rspesbca  3847  eliuni  4964  iuneqconst  4970  brralrspcev  5170  wefrc  5635  wereu2  5638  xpdifid  6144  frpomin  6316  onfr  6374  onelssex  6384  ordunidif  6385  eliman0  6901  dffv2  6959  elrnrexdm  7064  eldmrexrn  7066  elabrex  7219  elabrexg  7220  elunirn2OLD  7230  f1elima  7241  fliftfun  7290  fliftval  7294  f1oiso2  7330  sorpssuni  7711  sorpssint  7712  onssmin  7771  onminex  7781  fimaproj  8117  frxp3  8133  poseq  8140  tfrlem12  8360  seqomlem2  8422  oawordeulem  8521  oaass  8528  odi  8546  omass  8547  omeulem1  8549  oen0  8553  oelim2  8562  oeeulem  8568  nnawordex  8604  nnaordex2  8606  eldifsucnn  8631  cofon1  8639  cofon2  8640  naddcllem  8643  naddunif  8660  boxcutc  8917  0fi  9016  snfi  9017  snfiOLD  9018  rexdif1en  9128  rexdif1enOLD  9129  findcard  9133  nnfi  9137  pssnn  9138  unfi  9141  onfin  9185  dif1ennnALT  9229  frfi  9239  fisupg  9242  nnsdomg  9253  nnsdomgOLD  9254  pwfir  9273  prfi  9281  fissuni  9315  fipreima  9316  finsschain  9317  indexfi  9318  marypha1lem  9391  eqsup  9414  supmax  9426  fisup2g  9427  fisupcl  9428  supisoex  9433  infmin  9454  fiinfg  9459  fiinf2g  9460  wofib  9505  wemaplem2  9507  card2inf  9515  brwdom2  9533  cnfcom3clem  9665  ssttrcl  9675  ttrcltr  9676  trcl  9688  frmin  9709  r1ordg  9738  r1pwss  9744  tz9.12lem3  9749  tz9.12  9750  r1elwf  9756  tcrank  9844  scottex  9845  scott0  9846  isnumi  9906  onsdom  9956  ondomen  9997  infpwfien  10022  cardaleph  10049  infenaleph  10051  alephfplem4  10067  alephfp2  10069  dfac2b  10091  ackbij1lem18  10196  ackbij1  10197  cflem  10205  cflemOLD  10206  cflecard  10213  cfsuc  10217  cfflb  10219  cofsmo  10229  coftr  10233  fin23lem7  10276  fin23lem11  10277  enfin2i  10281  fin23lem26  10285  isf32lem5  10317  isf34lem4  10337  isfin1-3  10346  fin1a2lem7  10366  axdc3lem4  10413  ttukeylem7  10475  iunfo  10499  ficard  10525  pwcfsdom  10543  fpwwe2lem11  10601  wunex  10699  eltsk2g  10711  grur1  10780  axgroth6  10788  inaprc  10796  nqereu  10889  archnq  10940  genpnmax  10967  ltexpri  11003  prlem936  11007  recexpr  11011  supexpr  11014  negexsr  11062  recexsrlem  11063  recexsr  11067  supsrlem  11071  axrnegex  11122  axrrecex  11123  axpre-sup  11129  1re  11181  dedekind  11344  dedekindle  11345  cnegex  11362  cnegex2  11363  recex  11817  receu  11830  fiminre2  12138  cju  12189  nn2ge  12220  nominpos  12426  zdiv  12611  btwnz  12644  uzwo  12877  ublbneg  12899  lbzbi  12902  zsupss  12903  uzsupss  12906  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem4  12946  rpnnen1lem5  12947  z2ge  13165  qbtwnre  13166  qbtwnxr  13167  xralrple  13172  xrsupsslem  13274  xrinfmsslem  13275  supxrpnf  13285  icc0  13361  uzsup  13832  expnbnd  14204  expmulnbnd  14207  hashkf  14304  hashdom  14351  iswrdi  14489  rtrclreclem1  15030  rtrclreclem2  15032  rtrclreclem3  15033  01sqrex  15222  resqrex  15223  sqrtneg  15240  abs1m  15309  rexanuz  15319  rexuz3  15322  rexuzre  15326  sqreu  15334  o1lo1  15510  climconst  15516  rlimclim1  15518  climshftlem  15547  rlimo1  15590  lo1add  15600  lo1mul  15601  lo1le  15625  isercoll  15641  serf0  15654  zsum  15691  fsum  15693  fsumcvg3  15702  mertenslem1  15857  ntrivcvgn0  15871  ntrivcvgmullem  15874  zprod  15910  fprod  15914  fprodntriv  15915  dvdsval2  16232  dvds0lem  16243  dvds1lem  16244  dvds2lem  16245  odd2np1lem  16317  odd2np1  16318  opeo  16342  omeo  16343  divalglem9  16378  gcdcllem3  16478  lcmcllem  16573  qredeu  16635  exprmfct  16681  isprm5  16684  odzcllem  16770  reumodprminv  16782  modprm0  16783  nnnn0modprm0  16784  pythagtriplem19  16811  pcprmpw2  16860  pockthi  16885  infpnlem2  16889  vdwlem2  16960  vdwlem10  16968  vdwlem13  16971  ramub1lem1  17004  cshwrepswhash1  17080  imasleval  17511  mreexexlem3d  17614  mreexexlem4d  17615  iscatd  17641  cat1  18066  poslubd  18379  fpwipodrs  18506  ismgmid2  18602  mgmidsssn0  18606  gsumval2a  18619  ismndd  18690  isgrpd2  18895  isgrpd  18897  imasgrp2  18994  mhmmnd  19003  ghmgrp  19005  gaorber  19247  orbsta  19252  cayleyth  19352  pmtrdifel  19417  pmtrdifwrdel  19422  pmtrdifwrdel2  19423  psgnunilem2  19432  psgnunilem3  19433  psgnvalii  19446  pgpfi1  19532  sylow1lem3  19537  sylow1lem5  19539  pgpfi  19542  sylow2alem2  19555  efgredeu  19689  lt6abl  19832  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfac1lem5  20018  pgpfaclem1  20020  pgpfaclem3  20022  ablfaclem2  20025  dvdsrmul  20280  dvdsr01  20287  irredrmul  20343  rhmdvdsr  20424  rgspnval  20528  rgspncl  20529  lspf  20887  lspval  20888  lssats2  20913  lspfixed  21045  lspsolvlem  21059  zringlpir  21384  pzriprnglem13  21410  zncyg  21465  cygth  21488  frlmup4  21717  aspval  21789  evlseu  21997  fiinbas  22846  topbas  22866  pptbas  22902  clsval  22931  elcls  22967  neiint  22998  neips  23007  opnneissb  23008  opnssneib  23009  innei  23019  neiptopnei  23026  restbas  23052  neitr  23074  pnfnei  23114  mnfnei  23115  lmconst  23155  iscnp4  23157  cncnpi  23172  cnconst2  23177  cnprest  23183  cnpdis  23187  nrmsep  23251  regsep2  23270  cmpcovf  23285  cmpsub  23294  cmpcld  23296  hauscmplem  23300  conncompid  23325  2ndci  23342  2ndcsb  23343  2ndc1stc  23345  1stcrest  23347  2ndcctbss  23349  2ndcdisj  23350  2ndcomap  23352  2ndcsep  23353  dis2ndc  23354  restlly  23377  islly2  23378  hausllycmp  23388  cldllycmp  23389  lly1stc  23390  dislly  23391  ssref  23406  refref  23407  finlocfin  23414  dissnlocfin  23423  locfindis  23424  llycmpkgen2  23444  cmpkgen  23445  1stckgenlem  23447  elptr  23467  ptbasfi  23475  neitx  23501  ptpjopn  23506  txcnp  23514  ptcnplem  23515  txlly  23530  txnlly  23531  txtube  23534  txcmplem1  23535  tx1stc  23544  txkgen  23546  xkococnlem  23553  txconn  23583  tgqtop  23606  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  reghmph  23687  nrmhmph  23688  fbssfi  23731  opnfbas  23736  isfil2  23750  fsubbas  23761  ssfg  23766  fgss2  23768  fbasrn  23778  filuni  23779  fgtr  23784  ssufl  23812  uffix  23815  elfm2  23842  elfm3  23844  imaelfm  23845  rnelfmlem  23846  rnelfm  23847  fmfnfmlem4  23851  fmfnfm  23852  fmco  23855  ufldom  23856  hausflim  23875  flimcls  23879  hauspwpwf1  23881  flffbas  23889  txflf  23900  fclscf  23919  fclsfnflim  23921  alexsubALTlem4  23944  alexsubALT  23945  tmdgsum2  23990  symgtgp  24000  subgntr  24001  opnsubg  24002  ghmcnp  24009  qustgpopn  24014  tsmsfbas  24022  tsmsxplem1  24047  ustexsym  24110  trust  24124  utoptop  24129  restutop  24132  restutopopn  24133  ustuqtop4  24139  utopsnneiplem  24142  iducn  24177  fmucnd  24186  cfilufg  24187  trcfilu  24188  neipcfilu  24190  imasdsf1olem  24268  blssps  24319  blss  24320  blssexps  24321  blssex  24322  ssblex  24323  blin2  24324  neibl  24396  blcld  24400  metss2  24407  stdbdmopn  24413  met1stc  24416  met2ndci  24417  metrest  24419  prdsxmslem2  24424  metcnp3  24435  metustexhalf  24451  metustfbas  24452  cfilucfil  24454  restmetu  24465  dscopn  24468  ngptgp  24531  nlmvscnlem1  24581  tgioo  24691  tgqioo  24695  xrsmopn  24708  zcld  24709  recld2  24710  zdis  24712  icccmplem1  24718  icccmplem2  24719  xmetdcn2  24733  addcnlem  24760  xrhmeo  24851  cnheibor  24861  cnllycmp  24862  lebnumlem3  24869  lebnum  24870  xlebnum  24871  lebnumii  24872  elpi1i  24953  ipcnlem1  25152  lmnn  25170  iscfil3  25180  cfilres  25203  flimcfil  25221  bcthlem4  25234  bcthlem5  25235  minveclem4c  25332  minveclem2  25333  minveclem3b  25335  minveclem3  25336  minveclem4  25339  minveclem6  25341  ivthlem2  25360  ivth  25362  ivthle  25364  ivthle2  25365  elovolmr  25384  ovolunlem1  25405  ovoliunlem2  25411  ovolicc1  25424  iundisj  25456  iunmbl2  25465  dyadmbllem  25507  volivth  25515  mbflimsup  25574  i1faddlem  25601  i1fmullem  25602  itg2lr  25638  itg2monolem1  25658  limcnlp  25786  ellimc3  25787  limcflf  25789  limciun  25802  rollelem  25900  c1lip1  25909  lhop1lem  25925  ply1divex  26049  ig1peu  26087  elply2  26108  coeeq  26139  plydivlem3  26210  plydivlem4  26211  elqaalem3  26236  qaa  26238  iaa  26240  aareccl  26241  aannenlem2  26244  aalioulem2  26248  aalioulem3  26249  aalioulem5  26251  aalioulem6  26252  aaliou  26253  aaliou2  26255  aaliou3lem8  26260  ulmshftlem  26305  reeff1o  26364  pilem2  26369  pilem3  26370  efif1olem2  26459  efopn  26574  cxpcn3lem  26664  cxpeq  26674  dcubic2  26761  quart  26778  xrlimcnp  26885  ftalem5  26994  ftalem7  26996  sgmnncl  27064  dvdsppwf1o  27103  musum  27108  perfect  27149  dchrptlem1  27182  dchrptlem2  27183  dchrpt  27185  bpos1lem  27200  lgsqrlem4  27267  lgsdchrval  27272  2sqblem  27349  dchrisumlem3  27409  chpdifbndlem2  27472  pntrsumbnd2  27485  pntpbnd1  27504  pntpbnd2  27505  pntpbnd  27506  pntibndlem2  27509  pntibndlem3  27510  pntleme  27526  pntlem3  27527  elno2  27573  sltval2  27575  noreson  27579  sltres  27581  noseponlem  27583  nolesgn2o  27590  nogesgn1o  27592  nodense  27611  nosupfv  27625  nosupres  27626  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinffv  27640  noinfres  27641  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2lem1  27649  noetasuplem4  27655  noetainflem4  27659  noetalem2  27661  cuteq0  27751  cuteq1  27753  oldlim  27805  cofcutrtime  27842  cofss  27845  coiniss  27846  cutlt  27847  cutmax  27849  cutmin  27850  negsex  27956  negsfo  27966  norecdiv  28100  divs1  28114  precsexlem11  28126  precsex  28127  recsex  28128  elons2d  28167  onscutlt  28172  n0ons  28235  bdayn0sf1o  28266  dfnns2  28268  pw2recs  28330  halfcut  28340  0reno  28355  readdscl  28357  axtgcont  28403  tgcgrxfr  28452  legid  28521  btwnleg  28522  leg0  28526  tghilberti1  28571  tglnpt2  28575  colline  28583  mirreu3  28588  isperp2  28649  colperpex  28667  lnopp2hpgb  28697  hpgerlem  28699  brbtwn  28833  brcgr  28834  brbtwn2  28839  axpasch  28875  axlowdimlem14  28889  axlowdim2  28894  axcontlem2  28899  axcontlem4  28901  axcontlem8  28905  axcontlem10  28907  axcontlem12  28909  fusgrn0degnn0  29434  friendshipgt3  30334  lpni  30416  isgrpoi  30434  vacn  30630  smcnlem  30633  nmosetn0  30701  nmoolb  30707  nmobndi  30711  nmoo0  30727  nmlno0lem  30729  isblo3i  30737  blo3i  30738  blocnilem  30740  ubthlem1  30806  minvecolem2  30811  minvecolem3  30812  minvecolem4c  30815  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  norm1exi  31186  occl  31240  spanval  31269  spancl  31272  shsval2i  31323  ococin  31344  pjoml6i  31525  nmopsetn0  31801  nmfnsetn0  31814  nmoplb  31843  nmfnlb  31860  nmop0  31922  nmfn0  31923  nmlnop0iALT  31931  nmopun  31950  nmcexi  31962  lnconi  31969  lnopcnbd  31972  lnfncnbd  31993  riesz3i  31998  riesz1  32001  cnlnadjlem2  32004  cnlnadjlem8  32010  cnlnadjlem9  32011  adjbd1o  32021  branmfn  32041  opsqrlem1  32076  pjnmopi  32084  strlem1  32186  stri  32193  hstri  32201  cvcon3  32220  cvnbtwn  32222  superpos  32290  shatomici  32294  atcvat4i  32333  mdsymlem2  32340  cdj1i  32369  cdj3i  32377  rexunirn  32428  foresf1o  32440  iundisjf  32525  aciunf1lem  32593  fnpreimac  32602  fgreu  32603  fcnvgreu  32604  xrge0infss  32690  ssnnssfz  32717  iundisjfi  32726  indf1ofs  32796  xreceu  32849  rexdiv  32853  isarchi3  33148  archirngz  33150  archiabllem2a  33155  0nellinds  33348  qtophaus  33833  reff  33836  locfinreflem  33837  cmpcref  33847  dispcmp  33856  tpr2rico  33909  pnfneige0  33948  qqhucn  33989  rrhre  34018  esumcst  34060  esumpcvgval  34075  dmsigagen  34141  rossros  34177  dya2icoseg  34275  dya2iocnrect  34279  dya2iocuni  34281  eulerpartlemgvv  34374  dstfrvunirn  34473  ballotlem4  34497  ballotlemic  34505  ballotlem1c  34506  ballotlemrc  34529  signsw0g  34554  signswmnd  34555  prodfzo03  34601  tgoldbachgt  34661  onvf1odlem4  35100  loop1cycl  35131  umgr2cycllem  35134  umgr2cycl  35135  subfacp1lem3  35176  erdsze2lem2  35198  cnpconn  35224  txpconn  35226  ptpconn  35227  indispconn  35228  connpconn  35229  cvxpconn  35236  cnllysconn  35239  cvmsss2  35268  cvmcov2  35269  cvmopnlem  35272  cvmliftlem14  35291  cvmliftlem15  35292  cvmlift2lem11  35307  cvmlift2lem12  35308  cvmlift2lem13  35309  cvmlift3lem2  35314  cvmlift3lem6  35318  cvmlift3lem9  35321  mthmi  35571  r1peuqusdeg1  35637  br8  35750  br6  35751  br4  35752  dfon2lem9  35786  wzel  35819  wsuclem  35820  wsuclb  35823  imagesset  35948  fvtransport  36027  brcolinear  36054  brsegle  36103  seglerflx  36107  seglemin  36108  btwnsegle  36112  fvray  36136  fvline  36139  hilbert1.1  36149  elhf2  36170  0hf  36172  nn0prpwlem  36317  nn0prpw  36318  fness  36344  fneref  36345  fnessref  36352  refssfne  36353  neibastop2lem  36355  fnemeet1  36361  tailfb  36372  filnetlem4  36376  limsucncmpi  36440  taupilemrplb  37315  relowlssretop  37358  rdgellim  37371  matunitlindflem2  37618  ptrecube  37621  poimirlem4  37625  poimirlem17  37638  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem32  37653  heicant  37656  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  volsupnfl  37666  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  ftc1anclem5  37698  unirep  37715  cover2  37716  indexa  37734  frinfm  37736  sdclem1  37744  fdc  37746  incsequz  37749  caushft  37762  istotbnd3  37772  0totbnd  37774  sstotbnd2  37775  sstotbnd  37776  sstotbnd3  37777  isbnd3  37785  ssbnd  37789  equivbnd  37791  prdsbnd  37794  prdstotbnd  37795  cntotbnd  37797  heibor1lem  37810  heiborlem1  37812  heiborlem3  37814  heiborlem6  37817  heiborlem8  37819  bfplem2  37824  rrncmslem  37833  iccbnd  37841  opidonOLD  37853  exidres  37879  isrngod  37899  isgrpda  37956  isdrngo2  37959  igenval  38062  igenidl  38064  prtlem10  38865  lshpnel2N  38985  lsmsat  39008  lssatomic  39011  lcvnbtwn  39025  lfl1  39070  eqlkr  39099  lshpkrlem1  39110  lshpkrex  39118  cvrcon3b  39277  cvrat4  39444  3dim3  39470  ps-2  39479  llni  39509  llnle  39519  lplni  39533  lplnle  39541  lplnexllnN  39565  lvoli  39576  lnatexN  39780  elpaddn0  39801  pclfinN  39901  lhprelat3N  40041  4atexlemex2  40072  4atex  40077  4atex2-0aOLDN  40079  4atex2-0cOLDN  40081  lautcvr  40093  cdleme0ex1N  40224  cdleme50rnlem  40545  cdleme50ex  40560  cdlemg1cex  40589  cdlemkid5  40936  cdlemk  40975  tendoex  40976  cdleml5N  40981  cdlemm10N  41119  dih1dimatlem0  41329  dihjat1lem  41429  dvh3dim2  41449  dvh3dim3N  41450  dochkr1  41479  dochkr1OLDN  41480  lcfrvalsnN  41542  lcfrlem27  41570  lcfrlem37  41580  lcfr  41586  mapd1o  41649  mapdpglem23  41695  hdmap11lem2  41843  primrootsunit1  42092  zdivgd  42332  resubeu  42372  fidomncyc  42530  nacsfix  42707  mzpcompact2lem  42746  eldioph  42753  diophrw  42754  diophin  42767  rexrabdioph  42789  rexzrexnn0  42799  eldioph4b  42806  rencldnfilem  42815  irrapxlem5  42821  irrapxlem6  42822  pell1234qrdich  42856  pell14qrdich  42864  infmrgelbi  42873  pellqrex  42874  pellfundre  42876  pellfundlb  42879  rmxynorm  42914  congrep  42969  acongrep  42976  jm2.27  43004  fnwe2lem2  43047  islssfgi  43068  hbtlem2  43120  hbtlem4  43122  hbtlem5  43124  dgraaub  43144  mpaaeu  43146  aaitgo  43158  unielss  43214  onexgt  43236  onexomgt  43237  onexlimgt  43239  onexoegt  43240  oaordnr  43292  omnord1  43301  oenord1  43312  oaomoencom  43313  oenass  43315  tfsconcatfv2  43336  tfsconcatrn  43338  tfsconcatb0  43340  ofoafo  43352  naddcnffo  43360  oaun3lem1  43370  naddwordnexlem4  43397  sucomisnotcard  43540  clsk1independent  44042  0elaxnul  44980  pwclaxpow  44981  prclaxpr  44982  uniclaxun  44983  omssaxinf2  44985  wfac8prim  44999  restuni3  45119  iinssd  45132  founiiun  45180  wessf1ornlem  45186  founiiun0  45191  unirnmap  45209  dstregt0  45287  uzfissfz  45329  rpgtrecnn  45383  rexabslelem  45421  infrnmptle  45426  infxrunb3rnmpt  45431  infxrpnf  45449  supminfxr  45467  rexanuz2nf  45495  iooiinicc  45547  iooiinioc  45561  uzubioo  45570  climsuse  45613  islptre  45624  limsuppnfdlem  45706  climinf3  45721  limsupmnfuzlem  45731  limsupre3lem  45737  limsupre3uzlem  45740  0cnv  45747  liminfreuzlem  45807  cnrefiisplem  45834  icccncfext  45892  cncficcgt0  45893  dvbdfbdioo  45935  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem9  46014  stoweidlem14  46019  stoweidlem18  46023  stoweidlem21  46026  stoweidlem29  46034  stoweidlem34  46039  stoweidlem35  46040  stoweidlem39  46044  stoweidlem41  46046  stoweidlem45  46050  stoweidlem52  46057  stoweidlem55  46060  stoweidlem57  46062  stoweidlem60  46065  stirlinglem5  46083  stirlinglem13  46091  stirlinglem14  46092  fourierdlem16  46128  fourierdlem20  46132  fourierdlem21  46133  fourierdlem22  46134  fourierdlem25  46137  fourierdlem31  46143  fourierdlem39  46151  fourierdlem41  46153  fourierdlem42  46154  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem77  46188  fourierdlem81  46192  fourierdlem83  46194  fourierdlem103  46214  fourierdlem104  46215  elaa2lem  46238  etransclem47  46286  qndenserrnbl  46300  ioorrnopnlem  46309  ioorrnopnxrlem  46311  intsaluni  46334  salgencntex  46348  subsaliuncllem  46362  sge0resplit  46411  sge0seq  46451  sge0reuz  46452  nnfoctbdjlem  46460  meaiininclem  46491  hoicvrrex  46561  ovnlecvr  46563  ovnlerp  46567  hoidmv1lelem2  46597  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  ovnlecvr2  46615  hoiqssbl  46630  ovolval4lem2  46655  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  iinhoiicclem  46678  smfinflem  46822  smflimsuplem7  46831  sprsymrelfolem2  47498  perfectALTV  47728  9gbo  47779  11gbo  47780  nnsum3primes4  47793  nnsum3primesprm  47795  ssnn0ssfz  48341  lincsumcl  48424  lincscmcl  48425  zlmodzxzldep  48497  ldepsnlinc  48501  line2ylem  48744  line2xlem  48746  sepfsepc  48920  lubsscl  48952  glbsscl  48953  nelsubc3lem  49063  cnelsubclem  49596  aacllem  49794