Theorem rspcev 3564

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062

This theorem is referenced by:  rspcedvdw  3567  rspceaimv  3570  rspc2ev  3577  rspc3ev  3581  rspceeqv  3587  reu6i  3674  rspesbca  3819  eliuni  4939  iuneqconst  4945  brralrspcev  5145  wefrc  5625  wereu2  5628  xpdifid  6132  frpomin  6304  onfr  6362  onelssex  6372  ordunidif  6373  eliman0  6877  dffv2  6935  elrnrexdm  7041  eldmrexrn  7043  elabrex  7197  elabrexg  7198  f1elima  7218  fliftfun  7267  fliftval  7271  f1oiso2  7307  sorpssuni  7686  sorpssint  7687  onssmin  7746  onminex  7756  fimaproj  8085  frxp3  8101  poseq  8108  tfrlem12  8328  seqomlem2  8390  oawordeulem  8489  oaass  8496  odi  8514  omass  8515  omeulem1  8517  oen0  8522  oelim2  8531  oeeulem  8537  nnawordex  8573  nnaordex2  8575  eldifsucnn  8600  cofon1  8608  cofon2  8609  naddcllem  8612  naddunif  8629  boxcutc  8889  0fi  8989  snfi  8990  rexdif1en  9095  findcard  9098  nnfi  9102  pssnn  9103  unfi  9105  onfin  9149  dif1ennnALT  9187  frfi  9195  fisupg  9198  nnsdomg  9209  pwfir  9227  prfi  9234  fissuni  9267  fipreima  9268  finsschain  9269  indexfi  9270  marypha1lem  9346  eqsup  9369  supmax  9381  fisup2g  9382  fisupcl  9383  supisoex  9388  infmin  9409  fiinfg  9414  fiinf2g  9415  wofib  9460  wemaplem2  9462  card2inf  9470  brwdom2  9488  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  trcl  9649  frmin  9673  r1ordg  9702  r1pwss  9708  tz9.12lem3  9713  tz9.12  9714  r1elwf  9720  tcrank  9808  scottex  9809  scott0  9810  isnumi  9870  onsdom  9920  ondomen  9959  infpwfien  9984  cardaleph  10011  infenaleph  10013  alephfplem4  10029  alephfp2  10031  dfac2b  10053  ackbij1lem18  10158  ackbij1  10159  cflem  10167  cflemOLD  10168  cflecard  10175  cfsuc  10179  cfflb  10181  cofsmo  10191  coftr  10195  fin23lem7  10238  fin23lem11  10239  enfin2i  10243  fin23lem26  10247  isf32lem5  10279  isf34lem4  10299  isfin1-3  10308  fin1a2lem7  10328  axdc3lem4  10375  ttukeylem7  10437  iunfo  10461  ficard  10487  pwcfsdom  10506  fpwwe2lem11  10564  wunex  10662  eltsk2g  10674  grur1  10743  axgroth6  10751  inaprc  10759  nqereu  10852  archnq  10903  genpnmax  10930  ltexpri  10966  prlem936  10970  recexpr  10974  supexpr  10977  negexsr  11025  recexsrlem  11026  recexsr  11030  supsrlem  11034  axrnegex  11085  axrrecex  11086  axpre-sup  11092  1re  11144  dedekind  11309  dedekindle  11310  cnegex  11327  cnegex2  11328  recex  11782  receu  11795  fiminre2  12104  cju  12155  nn2ge  12204  nominpos  12414  zdiv  12599  btwnz  12632  uzwo  12861  ublbneg  12883  lbzbi  12886  zsupss  12887  uzsupss  12890  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem4  12930  rpnnen1lem5  12931  z2ge  13150  qbtwnre  13151  qbtwnxr  13152  xralrple  13157  xrsupsslem  13259  xrinfmsslem  13260  supxrpnf  13270  icc0  13346  uzsup  13822  expnbnd  14194  expmulnbnd  14197  hashkf  14294  hashdom  14341  iswrdi  14479  rtrclreclem1  15019  rtrclreclem2  15021  rtrclreclem3  15022  01sqrex  15211  resqrex  15212  sqrtneg  15229  abs1m  15298  rexanuz  15308  rexuz3  15311  rexuzre  15315  sqreu  15323  o1lo1  15499  climconst  15505  rlimclim1  15507  climshftlem  15536  rlimo1  15579  lo1add  15589  lo1mul  15590  lo1le  15614  isercoll  15630  serf0  15643  zsum  15680  fsum  15682  fsumcvg3  15691  mertenslem1  15849  ntrivcvgn0  15863  ntrivcvgmullem  15866  zprod  15902  fprod  15906  fprodntriv  15907  dvdsval2  16224  dvds0lem  16235  dvds1lem  16236  dvds2lem  16237  odd2np1lem  16309  odd2np1  16310  opeo  16334  omeo  16335  divalglem9  16370  gcdcllem3  16470  lcmcllem  16565  qredeu  16627  exprmfct  16674  isprm5  16677  odzcllem  16763  reumodprminv  16775  modprm0  16776  nnnn0modprm0  16777  pythagtriplem19  16804  pcprmpw2  16853  pockthi  16878  infpnlem2  16882  vdwlem2  16953  vdwlem10  16961  vdwlem13  16964  ramub1lem1  16997  cshwrepswhash1  17073  imasleval  17505  mreexexlem3d  17612  mreexexlem4d  17613  iscatd  17639  cat1  18064  poslubd  18377  fpwipodrs  18506  ismgmid2  18636  mgmidsssn0  18640  gsumval2a  18653  ismndd  18724  isgrpd2  18932  isgrpd  18934  imasgrp2  19031  mhmmnd  19040  ghmgrp  19042  gaorber  19283  orbsta  19288  cayleyth  19390  pmtrdifel  19455  pmtrdifwrdel  19460  pmtrdifwrdel2  19461  psgnunilem2  19470  psgnunilem3  19471  psgnvalii  19484  pgpfi1  19570  sylow1lem3  19575  sylow1lem5  19577  pgpfi  19580  sylow2alem2  19593  efgredeu  19727  lt6abl  19870  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfaclem1  20058  pgpfaclem3  20060  ablfaclem2  20063  dvdsrmul  20344  dvdsr01  20351  irredrmul  20407  rhmdvdsr  20485  rgspnval  20589  rgspncl  20590  lspf  20969  lspval  20970  lssats2  20995  lspfixed  21126  lspsolvlem  21140  zringlpir  21447  pzriprnglem13  21473  zncyg  21528  cygth  21551  frlmup4  21781  aspval  21852  evlseu  22061  fiinbas  22917  topbas  22937  pptbas  22973  clsval  23002  elcls  23038  neiint  23069  neips  23078  opnneissb  23079  opnssneib  23080  innei  23090  neiptopnei  23097  restbas  23123  neitr  23145  pnfnei  23185  mnfnei  23186  lmconst  23226  iscnp4  23228  cncnpi  23243  cnconst2  23248  cnprest  23254  cnpdis  23258  nrmsep  23322  regsep2  23341  cmpcovf  23356  cmpsub  23365  cmpcld  23367  hauscmplem  23371  conncompid  23396  2ndci  23413  2ndcsb  23414  2ndc1stc  23416  1stcrest  23418  2ndcctbss  23420  2ndcdisj  23421  2ndcomap  23423  2ndcsep  23424  dis2ndc  23425  restlly  23448  islly2  23449  hausllycmp  23459  cldllycmp  23460  lly1stc  23461  dislly  23462  ssref  23477  refref  23478  finlocfin  23485  dissnlocfin  23494  locfindis  23495  llycmpkgen2  23515  cmpkgen  23516  1stckgenlem  23518  elptr  23538  ptbasfi  23546  neitx  23572  ptpjopn  23577  txcnp  23585  ptcnplem  23586  txlly  23601  txnlly  23602  txtube  23605  txcmplem1  23606  tx1stc  23615  txkgen  23617  xkococnlem  23624  txconn  23654  tgqtop  23677  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  reghmph  23758  nrmhmph  23759  fbssfi  23802  opnfbas  23807  isfil2  23821  fsubbas  23832  ssfg  23837  fgss2  23839  fbasrn  23849  filuni  23850  fgtr  23855  ssufl  23883  uffix  23886  elfm2  23913  elfm3  23915  imaelfm  23916  rnelfmlem  23917  rnelfm  23918  fmfnfmlem4  23922  fmfnfm  23923  fmco  23926  ufldom  23927  hausflim  23946  flimcls  23950  hauspwpwf1  23952  flffbas  23960  txflf  23971  fclscf  23990  fclsfnflim  23992  alexsubALTlem4  24015  alexsubALT  24016  tmdgsum2  24061  symgtgp  24071  subgntr  24072  opnsubg  24073  ghmcnp  24080  qustgpopn  24085  tsmsfbas  24093  tsmsxplem1  24118  ustexsym  24181  trust  24194  utoptop  24199  restutop  24202  restutopopn  24203  ustuqtop4  24209  utopsnneiplem  24212  iducn  24247  fmucnd  24256  cfilufg  24257  trcfilu  24258  neipcfilu  24260  imasdsf1olem  24338  blssps  24389  blss  24390  blssexps  24391  blssex  24392  ssblex  24393  blin2  24394  neibl  24466  blcld  24470  metss2  24477  stdbdmopn  24483  met1stc  24486  met2ndci  24487  metrest  24489  prdsxmslem2  24494  metcnp3  24505  metustexhalf  24521  metustfbas  24522  cfilucfil  24524  restmetu  24535  dscopn  24538  ngptgp  24601  nlmvscnlem1  24651  tgioo  24761  tgqioo  24765  xrsmopn  24778  zcld  24779  recld2  24780  zdis  24782  icccmplem1  24788  icccmplem2  24789  xmetdcn2  24803  addcnlem  24830  xrhmeo  24913  cnheibor  24922  cnllycmp  24923  lebnumlem3  24930  lebnum  24931  xlebnum  24932  lebnumii  24933  elpi1i  25013  ipcnlem1  25212  lmnn  25230  iscfil3  25240  cfilres  25263  flimcfil  25281  bcthlem4  25294  bcthlem5  25295  minveclem4c  25392  minveclem2  25393  minveclem3b  25395  minveclem3  25396  minveclem4  25399  minveclem6  25401  ivthlem2  25419  ivth  25421  ivthle  25423  ivthle2  25424  elovolmr  25443  ovolunlem1  25464  ovoliunlem2  25470  ovolicc1  25483  iundisj  25515  iunmbl2  25524  dyadmbllem  25566  volivth  25574  mbflimsup  25633  i1faddlem  25660  i1fmullem  25661  itg2lr  25697  itg2monolem1  25717  limcnlp  25845  ellimc3  25846  limcflf  25848  limciun  25861  rollelem  25956  c1lip1  25964  lhop1lem  25980  ply1divex  26102  ig1peu  26140  elply2  26161  coeeq  26192  plydivlem3  26261  plydivlem4  26262  elqaalem3  26287  qaa  26289  iaa  26291  aareccl  26292  aannenlem2  26295  aalioulem2  26299  aalioulem3  26300  aalioulem5  26302  aalioulem6  26303  aaliou  26304  aaliou2  26306  aaliou3lem8  26311  ulmshftlem  26354  reeff1o  26412  pilem2  26417  pilem3  26418  efif1olem2  26507  efopn  26622  cxpcn3lem  26711  cxpeq  26721  dcubic2  26808  quart  26825  xrlimcnp  26932  ftalem5  27040  ftalem7  27042  sgmnncl  27110  dvdsppwf1o  27149  musum  27154  perfect  27194  dchrptlem1  27227  dchrptlem2  27228  dchrpt  27230  bpos1lem  27245  lgsqrlem4  27312  lgsdchrval  27317  2sqblem  27394  dchrisumlem3  27454  chpdifbndlem2  27517  pntrsumbnd2  27530  pntpbnd1  27549  pntpbnd2  27550  pntpbnd  27551  pntibndlem2  27554  pntibndlem3  27555  pntleme  27571  pntlem3  27572  elno2  27618  ltsval2  27620  noreson  27624  ltsres  27626  noseponlem  27628  nolesgn2o  27635  nogesgn1o  27637  nodense  27656  nosupfv  27670  nosupres  27671  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  noetalem2  27706  cuteq0  27807  cuteq1  27809  oldlim  27879  bdayiun  27907  cofcutrtime  27919  cofss  27922  coiniss  27923  cutlt  27924  cutmax  27926  cutmin  27927  negsex  28035  negsfo  28045  norecdiv  28182  divs1  28196  precsexlem11  28209  precsex  28210  recsex  28211  elons2d  28251  oncutlt  28256  n0on  28328  bdayn0sf1o  28362  dfnns2  28364  zsoring  28401  pw2recs  28430  halfcut  28450  0reno  28488  1reno  28489  readdscl  28491  axtgcont  28537  tgcgrxfr  28586  legid  28655  btwnleg  28656  leg0  28660  tghilberti1  28705  tglnpt2  28709  colline  28717  mirreu3  28722  isperp2  28783  colperpex  28801  lnopp2hpgb  28831  hpgerlem  28833  brbtwn  28968  brcgr  28969  brbtwn2  28974  axpasch  29010  axlowdimlem14  29024  axlowdim2  29029  axcontlem2  29034  axcontlem4  29036  axcontlem8  29040  axcontlem10  29042  axcontlem12  29044  fusgrn0degnn0  29568  friendshipgt3  30468  lpni  30551  isgrpoi  30569  vacn  30765  smcnlem  30768  nmosetn0  30836  nmoolb  30842  nmobndi  30846  nmoo0  30862  nmlno0lem  30864  isblo3i  30872  blo3i  30873  blocnilem  30875  ubthlem1  30941  minvecolem2  30946  minvecolem3  30947  minvecolem4c  30950  minvecolem4  30951  minvecolem5  30952  minvecolem6  30953  norm1exi  31321  occl  31375  spanval  31404  spancl  31407  shsval2i  31458  ococin  31479  pjoml6i  31660  nmopsetn0  31936  nmfnsetn0  31949  nmoplb  31978  nmfnlb  31995  nmop0  32057  nmfn0  32058  nmlnop0iALT  32066  nmopun  32085  nmcexi  32097  lnconi  32104  lnopcnbd  32107  lnfncnbd  32128  riesz3i  32133  riesz1  32136  cnlnadjlem2  32139  cnlnadjlem8  32145  cnlnadjlem9  32146  adjbd1o  32156  branmfn  32176  opsqrlem1  32211  pjnmopi  32219  strlem1  32321  stri  32328  hstri  32336  cvcon3  32355  cvnbtwn  32357  superpos  32425  shatomici  32429  atcvat4i  32468  mdsymlem2  32475  cdj1i  32504  cdj3i  32512  rexunirn  32561  foresf1o  32574  iundisjf  32659  aciunf1lem  32735  fnpreimac  32743  fgreu  32744  fcnvgreu  32745  xrge0infss  32833  ssnnssfz  32860  iundisjfi  32869  indf1ofs  32926  xreceu  32981  rexdiv  32985  isarchi3  33248  archirngz  33250  archiabllem2a  33255  0nellinds  33430  qtophaus  33980  reff  33983  locfinreflem  33984  cmpcref  33994  dispcmp  34003  tpr2rico  34056  pnfneige0  34095  qqhucn  34136  rrhre  34165  esumcst  34207  esumpcvgval  34222  dmsigagen  34288  rossros  34324  dya2icoseg  34421  dya2iocnrect  34425  dya2iocuni  34427  eulerpartlemgvv  34520  dstfrvunirn  34619  ballotlem4  34643  ballotlemic  34651  ballotlem1c  34652  ballotlemrc  34675  signsw0g  34700  signswmnd  34701  prodfzo03  34747  tgoldbachgt  34807  onvf1odlem4  35288  loop1cycl  35319  umgr2cycllem  35322  umgr2cycl  35323  subfacp1lem3  35364  erdsze2lem2  35386  cnpconn  35412  txpconn  35414  ptpconn  35415  indispconn  35416  connpconn  35417  cvxpconn  35424  cnllysconn  35427  cvmsss2  35456  cvmcov2  35457  cvmopnlem  35460  cvmliftlem14  35479  cvmliftlem15  35480  cvmlift2lem11  35495  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmlift3lem2  35502  cvmlift3lem6  35506  cvmlift3lem9  35509  mthmi  35759  r1peuqusdeg1  35825  br8  35938  br6  35939  br4  35940  dfon2lem9  35971  wzel  36004  wsuclem  36005  wsuclb  36008  imagesset  36135  fvtransport  36214  brcolinear  36241  brsegle  36290  seglerflx  36294  seglemin  36295  btwnsegle  36299  fvray  36323  fvline  36326  hilbert1.1  36336  elhf2  36357  0hf  36359  nn0prpwlem  36504  nn0prpw  36505  fness  36531  fneref  36532  fnessref  36539  refssfne  36540  neibastop2lem  36542  fnemeet1  36548  tailfb  36559  filnetlem4  36563  limsucncmpi  36627  ttctr  36675  dfttc2g  36688  taupilemrplb  37634  qdiff  37641  relowlssretop  37679  rdgellim  37692  matunitlindflem2  37938  ptrecube  37941  poimirlem4  37945  poimirlem17  37958  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem32  37973  heicant  37976  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  volsupnfl  37986  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem5  38018  unirep  38035  cover2  38036  indexa  38054  frinfm  38056  sdclem1  38064  fdc  38066  incsequz  38069  caushft  38082  istotbnd3  38092  0totbnd  38094  sstotbnd2  38095  sstotbnd  38096  sstotbnd3  38097  isbnd3  38105  ssbnd  38109  equivbnd  38111  prdsbnd  38114  prdstotbnd  38115  cntotbnd  38117  heibor1lem  38130  heiborlem1  38132  heiborlem3  38134  heiborlem6  38137  heiborlem8  38139  bfplem2  38144  rrncmslem  38153  iccbnd  38161  opidonOLD  38173  exidres  38199  isrngod  38219  isgrpda  38276  isdrngo2  38279  igenval  38382  igenidl  38384  prtlem10  39311  lshpnel2N  39431  lsmsat  39454  lssatomic  39457  lcvnbtwn  39471  lfl1  39516  eqlkr  39545  lshpkrlem1  39556  lshpkrex  39564  cvrcon3b  39723  cvrat4  39889  3dim3  39915  ps-2  39924  llni  39954  llnle  39964  lplni  39978  lplnle  39986  lplnexllnN  40010  lvoli  40021  lnatexN  40225  elpaddn0  40246  pclfinN  40346  lhprelat3N  40486  4atexlemex2  40517  4atex  40522  4atex2-0aOLDN  40524  4atex2-0cOLDN  40526  lautcvr  40538  cdleme0ex1N  40669  cdleme50rnlem  40990  cdleme50ex  41005  cdlemg1cex  41034  cdlemkid5  41381  cdlemk  41420  tendoex  41421  cdleml5N  41426  cdlemm10N  41564  dih1dimatlem0  41774  dihjat1lem  41874  dvh3dim2  41894  dvh3dim3N  41895  dochkr1  41924  dochkr1OLDN  41925  lcfrvalsnN  41987  lcfrlem27  42015  lcfrlem37  42025  lcfr  42031  mapd1o  42094  mapdpglem23  42140  hdmap11lem2  42288  primrootsunit1  42536  zdivgd  42769  resubeu  42809  fidomncyc  42980  nacsfix  43144  mzpcompact2lem  43183  eldioph  43190  diophrw  43191  diophin  43204  rexrabdioph  43222  rexzrexnn0  43232  eldioph4b  43239  rencldnfilem  43248  irrapxlem5  43254  irrapxlem6  43255  pell1234qrdich  43289  pell14qrdich  43297  infmrgelbi  43306  pellqrex  43307  pellfundre  43309  pellfundlb  43312  rmxynorm  43346  congrep  43401  acongrep  43408  jm2.27  43436  fnwe2lem2  43479  islssfgi  43500  hbtlem2  43552  hbtlem4  43554  hbtlem5  43556  dgraaub  43576  mpaaeu  43578  aaitgo  43590  unielss  43646  onexgt  43668  onexomgt  43669  onexlimgt  43671  onexoegt  43672  oaordnr  43724  omnord1  43733  oenord1  43744  oaomoencom  43745  oenass  43747  tfsconcatfv2  43768  tfsconcatrn  43770  tfsconcatb0  43772  ofoafo  43784  naddcnffo  43792  oaun3lem1  43802  naddwordnexlem4  43829  sucomisnotcard  43971  clsk1independent  44473  0elaxnul  45410  pwclaxpow  45411  prclaxpr  45412  uniclaxun  45413  omssaxinf2  45415  wfac8prim  45429  restuni3  45548  iinssd  45561  founiiun  45609  wessf1ornlem  45615  founiiun0  45620  unirnmap  45637  dstregt0  45715  uzfissfz  45756  rpgtrecnn  45809  rexabslelem  45846  infrnmptle  45851  infxrunb3rnmpt  45856  infxrpnf  45874  supminfxr  45892  rexanuz2nf  45920  iooiinicc  45972  iooiinioc  45986  uzubioo  45995  climsuse  46038  islptre  46049  limsuppnfdlem  46129  climinf3  46144  limsupmnfuzlem  46154  limsupre3lem  46160  limsupre3uzlem  46163  0cnv  46170  liminfreuzlem  46230  cnrefiisplem  46257  icccncfext  46315  cncficcgt0  46316  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem9  46437  stoweidlem14  46442  stoweidlem18  46446  stoweidlem21  46449  stoweidlem29  46457  stoweidlem34  46462  stoweidlem35  46463  stoweidlem39  46467  stoweidlem41  46469  stoweidlem45  46473  stoweidlem52  46480  stoweidlem55  46483  stoweidlem57  46485  stoweidlem60  46488  stirlinglem5  46506  stirlinglem13  46514  stirlinglem14  46515  fourierdlem16  46551  fourierdlem20  46555  fourierdlem21  46556  fourierdlem22  46557  fourierdlem25  46560  fourierdlem31  46566  fourierdlem39  46574  fourierdlem41  46576  fourierdlem42  46577  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem77  46611  fourierdlem81  46615  fourierdlem83  46617  fourierdlem103  46637  fourierdlem104  46638  elaa2lem  46661  etransclem47  46709  qndenserrnbl  46723  ioorrnopnlem  46732  ioorrnopnxrlem  46734  intsaluni  46757  salgencntex  46771  subsaliuncllem  46785  sge0resplit  46834  sge0seq  46874  sge0reuz  46875  nnfoctbdjlem  46883  meaiininclem  46914  hoicvrrex  46984  ovnlecvr  46986  ovnlerp  46990  hoidmv1lelem2  47020  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  ovnlecvr2  47038  hoiqssbl  47053  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  iinhoiicclem  47101  smfinflem  47245  smflimsuplem7  47254  nthrucw  47316  sprsymrelfolem2  47953  perfectALTV  48199  9gbo  48250  11gbo  48251  nnsum3primes4  48264  nnsum3primesprm  48266  ssnn0ssfz  48825  lincsumcl  48907  lincscmcl  48908  zlmodzxzldep  48980  ldepsnlinc  48984  line2ylem  49227  line2xlem  49229  sepfsepc  49403  lubsscl  49435  glbsscl  49436  nelsubc3lem  49545  cnelsubclem  50078  aacllem  50276