Theorem rspcev 3577

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 3570	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  rspcedvdw  3580  rspceb2dv  3581  rspceaimv  3583  rspc2ev  3590  rspc3ev  3594  rspceeqv  3600  reu6i  3688  rspesbca  3833  eliuni  4947  iuneqconst  4953  brralrspcev  5152  wefrc  5613  wereu2  5616  xpdifid  6117  frpomin  6288  onfr  6346  onelssex  6356  ordunidif  6357  eliman0  6860  dffv2  6918  elrnrexdm  7023  eldmrexrn  7025  elabrex  7178  elabrexg  7179  elunirn2OLD  7189  f1elima  7200  fliftfun  7249  fliftval  7253  f1oiso2  7289  sorpssuni  7668  sorpssint  7669  onssmin  7728  onminex  7738  fimaproj  8068  frxp3  8084  poseq  8091  tfrlem12  8311  seqomlem2  8373  oawordeulem  8472  oaass  8479  odi  8497  omass  8498  omeulem1  8500  oen0  8504  oelim2  8513  oeeulem  8519  nnawordex  8555  nnaordex2  8557  eldifsucnn  8582  cofon1  8590  cofon2  8591  naddcllem  8594  naddunif  8611  boxcutc  8868  0fi  8967  snfi  8968  snfiOLD  8969  rexdif1en  9074  findcard  9077  nnfi  9081  pssnn  9082  unfi  9085  onfin  9129  dif1ennnALT  9166  frfi  9174  fisupg  9177  nnsdomg  9188  pwfir  9206  prfi  9213  fissuni  9247  fipreima  9248  finsschain  9249  indexfi  9250  marypha1lem  9323  eqsup  9346  supmax  9358  fisup2g  9359  fisupcl  9360  supisoex  9365  infmin  9386  fiinfg  9391  fiinf2g  9392  wofib  9437  wemaplem2  9439  card2inf  9447  brwdom2  9465  cnfcom3clem  9601  ssttrcl  9611  ttrcltr  9612  trcl  9624  frmin  9645  r1ordg  9674  r1pwss  9680  tz9.12lem3  9685  tz9.12  9686  r1elwf  9692  tcrank  9780  scottex  9781  scott0  9782  isnumi  9842  onsdom  9892  ondomen  9931  infpwfien  9956  cardaleph  9983  infenaleph  9985  alephfplem4  10001  alephfp2  10003  dfac2b  10025  ackbij1lem18  10130  ackbij1  10131  cflem  10139  cflemOLD  10140  cflecard  10147  cfsuc  10151  cfflb  10153  cofsmo  10163  coftr  10167  fin23lem7  10210  fin23lem11  10211  enfin2i  10215  fin23lem26  10219  isf32lem5  10251  isf34lem4  10271  isfin1-3  10280  fin1a2lem7  10300  axdc3lem4  10347  ttukeylem7  10409  iunfo  10433  ficard  10459  pwcfsdom  10477  fpwwe2lem11  10535  wunex  10633  eltsk2g  10645  grur1  10714  axgroth6  10722  inaprc  10730  nqereu  10823  archnq  10874  genpnmax  10901  ltexpri  10937  prlem936  10941  recexpr  10945  supexpr  10948  negexsr  10996  recexsrlem  10997  recexsr  11001  supsrlem  11005  axrnegex  11056  axrrecex  11057  axpre-sup  11063  1re  11115  dedekind  11279  dedekindle  11280  cnegex  11297  cnegex2  11298  recex  11752  receu  11765  fiminre2  12073  cju  12124  nn2ge  12155  nominpos  12361  zdiv  12546  btwnz  12579  uzwo  12812  ublbneg  12834  lbzbi  12837  zsupss  12838  uzsupss  12841  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem4  12881  rpnnen1lem5  12882  z2ge  13100  qbtwnre  13101  qbtwnxr  13102  xralrple  13107  xrsupsslem  13209  xrinfmsslem  13210  supxrpnf  13220  icc0  13296  uzsup  13767  expnbnd  14139  expmulnbnd  14142  hashkf  14239  hashdom  14286  iswrdi  14424  rtrclreclem1  14964  rtrclreclem2  14966  rtrclreclem3  14967  01sqrex  15156  resqrex  15157  sqrtneg  15174  abs1m  15243  rexanuz  15253  rexuz3  15256  rexuzre  15260  sqreu  15268  o1lo1  15444  climconst  15450  rlimclim1  15452  climshftlem  15481  rlimo1  15524  lo1add  15534  lo1mul  15535  lo1le  15559  isercoll  15575  serf0  15588  zsum  15625  fsum  15627  fsumcvg3  15636  mertenslem1  15791  ntrivcvgn0  15805  ntrivcvgmullem  15808  zprod  15844  fprod  15848  fprodntriv  15849  dvdsval2  16166  dvds0lem  16177  dvds1lem  16178  dvds2lem  16179  odd2np1lem  16251  odd2np1  16252  opeo  16276  omeo  16277  divalglem9  16312  gcdcllem3  16412  lcmcllem  16507  qredeu  16569  exprmfct  16615  isprm5  16618  odzcllem  16704  reumodprminv  16716  modprm0  16717  nnnn0modprm0  16718  pythagtriplem19  16745  pcprmpw2  16794  pockthi  16819  infpnlem2  16823  vdwlem2  16894  vdwlem10  16902  vdwlem13  16905  ramub1lem1  16938  cshwrepswhash1  17014  imasleval  17445  mreexexlem3d  17552  mreexexlem4d  17553  iscatd  17579  cat1  18004  poslubd  18317  fpwipodrs  18446  ismgmid2  18542  mgmidsssn0  18546  gsumval2a  18559  ismndd  18630  isgrpd2  18835  isgrpd  18837  imasgrp2  18934  mhmmnd  18943  ghmgrp  18945  gaorber  19187  orbsta  19192  cayleyth  19294  pmtrdifel  19359  pmtrdifwrdel  19364  pmtrdifwrdel2  19365  psgnunilem2  19374  psgnunilem3  19375  psgnvalii  19388  pgpfi1  19474  sylow1lem3  19479  sylow1lem5  19481  pgpfi  19484  sylow2alem2  19497  efgredeu  19631  lt6abl  19774  pgpfac1lem3a  19957  pgpfac1lem3  19958  pgpfac1lem5  19960  pgpfaclem1  19962  pgpfaclem3  19964  ablfaclem2  19967  dvdsrmul  20249  dvdsr01  20256  irredrmul  20312  rhmdvdsr  20393  rgspnval  20497  rgspncl  20498  lspf  20877  lspval  20878  lssats2  20903  lspfixed  21035  lspsolvlem  21049  zringlpir  21374  pzriprnglem13  21400  zncyg  21455  cygth  21478  frlmup4  21708  aspval  21780  evlseu  21988  fiinbas  22837  topbas  22857  pptbas  22893  clsval  22922  elcls  22958  neiint  22989  neips  22998  opnneissb  22999  opnssneib  23000  innei  23010  neiptopnei  23017  restbas  23043  neitr  23065  pnfnei  23105  mnfnei  23106  lmconst  23146  iscnp4  23148  cncnpi  23163  cnconst2  23168  cnprest  23174  cnpdis  23178  nrmsep  23242  regsep2  23261  cmpcovf  23276  cmpsub  23285  cmpcld  23287  hauscmplem  23291  conncompid  23316  2ndci  23333  2ndcsb  23334  2ndc1stc  23336  1stcrest  23338  2ndcctbss  23340  2ndcdisj  23341  2ndcomap  23343  2ndcsep  23344  dis2ndc  23345  restlly  23368  islly2  23369  hausllycmp  23379  cldllycmp  23380  lly1stc  23381  dislly  23382  ssref  23397  refref  23398  finlocfin  23405  dissnlocfin  23414  locfindis  23415  llycmpkgen2  23435  cmpkgen  23436  1stckgenlem  23438  elptr  23458  ptbasfi  23466  neitx  23492  ptpjopn  23497  txcnp  23505  ptcnplem  23506  txlly  23521  txnlly  23522  txtube  23525  txcmplem1  23526  tx1stc  23535  txkgen  23537  xkococnlem  23544  txconn  23574  tgqtop  23597  kqreglem1  23626  kqreglem2  23627  kqnrmlem1  23628  kqnrmlem2  23629  reghmph  23678  nrmhmph  23679  fbssfi  23722  opnfbas  23727  isfil2  23741  fsubbas  23752  ssfg  23757  fgss2  23759  fbasrn  23769  filuni  23770  fgtr  23775  ssufl  23803  uffix  23806  elfm2  23833  elfm3  23835  imaelfm  23836  rnelfmlem  23837  rnelfm  23838  fmfnfmlem4  23842  fmfnfm  23843  fmco  23846  ufldom  23847  hausflim  23866  flimcls  23870  hauspwpwf1  23872  flffbas  23880  txflf  23891  fclscf  23910  fclsfnflim  23912  alexsubALTlem4  23935  alexsubALT  23936  tmdgsum2  23981  symgtgp  23991  subgntr  23992  opnsubg  23993  ghmcnp  24000  qustgpopn  24005  tsmsfbas  24013  tsmsxplem1  24038  ustexsym  24101  trust  24115  utoptop  24120  restutop  24123  restutopopn  24124  ustuqtop4  24130  utopsnneiplem  24133  iducn  24168  fmucnd  24177  cfilufg  24178  trcfilu  24179  neipcfilu  24181  imasdsf1olem  24259  blssps  24310  blss  24311  blssexps  24312  blssex  24313  ssblex  24314  blin2  24315  neibl  24387  blcld  24391  metss2  24398  stdbdmopn  24404  met1stc  24407  met2ndci  24408  metrest  24410  prdsxmslem2  24415  metcnp3  24426  metustexhalf  24442  metustfbas  24443  cfilucfil  24445  restmetu  24456  dscopn  24459  ngptgp  24522  nlmvscnlem1  24572  tgioo  24682  tgqioo  24686  xrsmopn  24699  zcld  24700  recld2  24701  zdis  24703  icccmplem1  24709  icccmplem2  24710  xmetdcn2  24724  addcnlem  24751  xrhmeo  24842  cnheibor  24852  cnllycmp  24853  lebnumlem3  24860  lebnum  24861  xlebnum  24862  lebnumii  24863  elpi1i  24944  ipcnlem1  25143  lmnn  25161  iscfil3  25171  cfilres  25194  flimcfil  25212  bcthlem4  25225  bcthlem5  25226  minveclem4c  25323  minveclem2  25324  minveclem3b  25326  minveclem3  25327  minveclem4  25330  minveclem6  25332  ivthlem2  25351  ivth  25353  ivthle  25355  ivthle2  25356  elovolmr  25375  ovolunlem1  25396  ovoliunlem2  25402  ovolicc1  25415  iundisj  25447  iunmbl2  25456  dyadmbllem  25498  volivth  25506  mbflimsup  25565  i1faddlem  25592  i1fmullem  25593  itg2lr  25629  itg2monolem1  25649  limcnlp  25777  ellimc3  25778  limcflf  25780  limciun  25793  rollelem  25891  c1lip1  25900  lhop1lem  25916  ply1divex  26040  ig1peu  26078  elply2  26099  coeeq  26130  plydivlem3  26201  plydivlem4  26202  elqaalem3  26227  qaa  26229  iaa  26231  aareccl  26232  aannenlem2  26235  aalioulem2  26239  aalioulem3  26240  aalioulem5  26242  aalioulem6  26243  aaliou  26244  aaliou2  26246  aaliou3lem8  26251  ulmshftlem  26296  reeff1o  26355  pilem2  26360  pilem3  26361  efif1olem2  26450  efopn  26565  cxpcn3lem  26655  cxpeq  26665  dcubic2  26752  quart  26769  xrlimcnp  26876  ftalem5  26985  ftalem7  26987  sgmnncl  27055  dvdsppwf1o  27094  musum  27099  perfect  27140  dchrptlem1  27173  dchrptlem2  27174  dchrpt  27176  bpos1lem  27191  lgsqrlem4  27258  lgsdchrval  27263  2sqblem  27340  dchrisumlem3  27400  chpdifbndlem2  27463  pntrsumbnd2  27476  pntpbnd1  27495  pntpbnd2  27496  pntpbnd  27497  pntibndlem2  27500  pntibndlem3  27501  pntleme  27517  pntlem3  27518  elno2  27564  sltval2  27566  noreson  27570  sltres  27572  noseponlem  27574  nolesgn2o  27581  nogesgn1o  27583  nodense  27602  nosupfv  27616  nosupres  27617  nosupbnd1lem3  27620  nosupbnd1lem5  27622  nosupbnd2lem1  27625  noinffv  27631  noinfres  27632  noinfbnd1lem3  27635  noinfbnd1lem5  27637  noinfbnd2lem1  27640  noetasuplem4  27646  noetainflem4  27650  noetalem2  27652  cuteq0  27746  cuteq1  27748  oldlim  27801  bdayiun  27829  cofcutrtime  27840  cofss  27843  coiniss  27844  cutlt  27845  cutmax  27847  cutmin  27848  negsex  27954  negsfo  27964  norecdiv  28098  divs1  28112  precsexlem11  28124  precsex  28125  recsex  28126  elons2d  28165  onscutlt  28170  n0ons  28233  bdayn0sf1o  28264  dfnns2  28266  zsoring  28301  pw2recs  28330  halfcut  28346  0reno  28366  readdscl  28368  axtgcont  28414  tgcgrxfr  28463  legid  28532  btwnleg  28533  leg0  28537  tghilberti1  28582  tglnpt2  28586  colline  28594  mirreu3  28599  isperp2  28660  colperpex  28678  lnopp2hpgb  28708  hpgerlem  28710  brbtwn  28844  brcgr  28845  brbtwn2  28850  axpasch  28886  axlowdimlem14  28900  axlowdim2  28905  axcontlem2  28910  axcontlem4  28912  axcontlem8  28916  axcontlem10  28918  axcontlem12  28920  fusgrn0degnn0  29445  friendshipgt3  30342  lpni  30424  isgrpoi  30442  vacn  30638  smcnlem  30641  nmosetn0  30709  nmoolb  30715  nmobndi  30719  nmoo0  30735  nmlno0lem  30737  isblo3i  30745  blo3i  30746  blocnilem  30748  ubthlem1  30814  minvecolem2  30819  minvecolem3  30820  minvecolem4c  30823  minvecolem4  30824  minvecolem5  30825  minvecolem6  30826  norm1exi  31194  occl  31248  spanval  31277  spancl  31280  shsval2i  31331  ococin  31352  pjoml6i  31533  nmopsetn0  31809  nmfnsetn0  31822  nmoplb  31851  nmfnlb  31868  nmop0  31930  nmfn0  31931  nmlnop0iALT  31939  nmopun  31958  nmcexi  31970  lnconi  31977  lnopcnbd  31980  lnfncnbd  32001  riesz3i  32006  riesz1  32009  cnlnadjlem2  32012  cnlnadjlem8  32018  cnlnadjlem9  32019  adjbd1o  32029  branmfn  32049  opsqrlem1  32084  pjnmopi  32092  strlem1  32194  stri  32201  hstri  32209  cvcon3  32228  cvnbtwn  32230  superpos  32298  shatomici  32302  atcvat4i  32341  mdsymlem2  32348  cdj1i  32377  cdj3i  32385  rexunirn  32436  foresf1o  32448  iundisjf  32533  aciunf1lem  32606  fnpreimac  32615  fgreu  32616  fcnvgreu  32617  xrge0infss  32704  ssnnssfz  32731  iundisjfi  32740  indf1ofs  32810  xreceu  32863  rexdiv  32867  isarchi3  33130  archirngz  33132  archiabllem2a  33137  0nellinds  33308  qtophaus  33809  reff  33812  locfinreflem  33813  cmpcref  33823  dispcmp  33832  tpr2rico  33885  pnfneige0  33924  qqhucn  33965  rrhre  33994  esumcst  34036  esumpcvgval  34051  dmsigagen  34117  rossros  34153  dya2icoseg  34251  dya2iocnrect  34255  dya2iocuni  34257  eulerpartlemgvv  34350  dstfrvunirn  34449  ballotlem4  34473  ballotlemic  34481  ballotlem1c  34482  ballotlemrc  34505  signsw0g  34530  signswmnd  34531  prodfzo03  34577  tgoldbachgt  34637  onvf1odlem4  35089  loop1cycl  35120  umgr2cycllem  35123  umgr2cycl  35124  subfacp1lem3  35165  erdsze2lem2  35187  cnpconn  35213  txpconn  35215  ptpconn  35216  indispconn  35217  connpconn  35218  cvxpconn  35225  cnllysconn  35228  cvmsss2  35257  cvmcov2  35258  cvmopnlem  35261  cvmliftlem14  35280  cvmliftlem15  35281  cvmlift2lem11  35296  cvmlift2lem12  35297  cvmlift2lem13  35298  cvmlift3lem2  35303  cvmlift3lem6  35307  cvmlift3lem9  35310  mthmi  35560  r1peuqusdeg1  35626  br8  35739  br6  35740  br4  35741  dfon2lem9  35775  wzel  35808  wsuclem  35809  wsuclb  35812  imagesset  35937  fvtransport  36016  brcolinear  36043  brsegle  36092  seglerflx  36096  seglemin  36097  btwnsegle  36101  fvray  36125  fvline  36128  hilbert1.1  36138  elhf2  36159  0hf  36161  nn0prpwlem  36306  nn0prpw  36307  fness  36333  fneref  36334  fnessref  36341  refssfne  36342  neibastop2lem  36344  fnemeet1  36350  tailfb  36361  filnetlem4  36365  limsucncmpi  36429  taupilemrplb  37304  relowlssretop  37347  rdgellim  37360  matunitlindflem2  37607  ptrecube  37610  poimirlem4  37614  poimirlem17  37627  poimirlem20  37630  poimirlem23  37633  poimirlem24  37634  poimirlem26  37636  poimirlem27  37637  poimirlem29  37639  poimirlem32  37642  heicant  37645  mblfinlem1  37647  mblfinlem2  37648  mblfinlem3  37649  mblfinlem4  37650  ismblfin  37651  volsupnfl  37655  itg2addnclem  37661  itg2addnclem3  37663  itg2addnc  37664  ftc1anclem5  37687  unirep  37704  cover2  37705  indexa  37723  frinfm  37725  sdclem1  37733  fdc  37735  incsequz  37738  caushft  37751  istotbnd3  37761  0totbnd  37763  sstotbnd2  37764  sstotbnd  37765  sstotbnd3  37766  isbnd3  37774  ssbnd  37778  equivbnd  37780  prdsbnd  37783  prdstotbnd  37784  cntotbnd  37786  heibor1lem  37799  heiborlem1  37801  heiborlem3  37803  heiborlem6  37806  heiborlem8  37808  bfplem2  37813  rrncmslem  37822  iccbnd  37830  opidonOLD  37842  exidres  37868  isrngod  37888  isgrpda  37945  isdrngo2  37948  igenval  38051  igenidl  38053  prtlem10  38854  lshpnel2N  38974  lsmsat  38997  lssatomic  39000  lcvnbtwn  39014  lfl1  39059  eqlkr  39088  lshpkrlem1  39099  lshpkrex  39107  cvrcon3b  39266  cvrat4  39432  3dim3  39458  ps-2  39467  llni  39497  llnle  39507  lplni  39521  lplnle  39529  lplnexllnN  39553  lvoli  39564  lnatexN  39768  elpaddn0  39789  pclfinN  39889  lhprelat3N  40029  4atexlemex2  40060  4atex  40065  4atex2-0aOLDN  40067  4atex2-0cOLDN  40069  lautcvr  40081  cdleme0ex1N  40212  cdleme50rnlem  40533  cdleme50ex  40548  cdlemg1cex  40577  cdlemkid5  40924  cdlemk  40963  tendoex  40964  cdleml5N  40969  cdlemm10N  41107  dih1dimatlem0  41317  dihjat1lem  41417  dvh3dim2  41437  dvh3dim3N  41438  dochkr1  41467  dochkr1OLDN  41468  lcfrvalsnN  41530  lcfrlem27  41558  lcfrlem37  41568  lcfr  41574  mapd1o  41637  mapdpglem23  41683  hdmap11lem2  41831  primrootsunit1  42080  zdivgd  42320  resubeu  42360  fidomncyc  42518  nacsfix  42695  mzpcompact2lem  42734  eldioph  42741  diophrw  42742  diophin  42755  rexrabdioph  42777  rexzrexnn0  42787  eldioph4b  42794  rencldnfilem  42803  irrapxlem5  42809  irrapxlem6  42810  pell1234qrdich  42844  pell14qrdich  42852  infmrgelbi  42861  pellqrex  42862  pellfundre  42864  pellfundlb  42867  rmxynorm  42901  congrep  42956  acongrep  42963  jm2.27  42991  fnwe2lem2  43034  islssfgi  43055  hbtlem2  43107  hbtlem4  43109  hbtlem5  43111  dgraaub  43131  mpaaeu  43133  aaitgo  43145  unielss  43201  onexgt  43223  onexomgt  43224  onexlimgt  43226  onexoegt  43227  oaordnr  43279  omnord1  43288  oenord1  43299  oaomoencom  43300  oenass  43302  tfsconcatfv2  43323  tfsconcatrn  43325  tfsconcatb0  43327  ofoafo  43339  naddcnffo  43347  oaun3lem1  43357  naddwordnexlem4  43384  sucomisnotcard  43527  clsk1independent  44029  0elaxnul  44967  pwclaxpow  44968  prclaxpr  44969  uniclaxun  44970  omssaxinf2  44972  wfac8prim  44986  restuni3  45106  iinssd  45119  founiiun  45167  wessf1ornlem  45173  founiiun0  45178  unirnmap  45196  dstregt0  45274  uzfissfz  45316  rpgtrecnn  45369  rexabslelem  45407  infrnmptle  45412  infxrunb3rnmpt  45417  infxrpnf  45435  supminfxr  45453  rexanuz2nf  45481  iooiinicc  45533  iooiinioc  45547  uzubioo  45556  climsuse  45599  islptre  45610  limsuppnfdlem  45692  climinf3  45707  limsupmnfuzlem  45717  limsupre3lem  45723  limsupre3uzlem  45726  0cnv  45733  liminfreuzlem  45793  cnrefiisplem  45820  icccncfext  45878  cncficcgt0  45879  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem9  46000  stoweidlem14  46005  stoweidlem18  46009  stoweidlem21  46012  stoweidlem29  46020  stoweidlem34  46025  stoweidlem35  46026  stoweidlem39  46030  stoweidlem41  46032  stoweidlem45  46036  stoweidlem52  46043  stoweidlem55  46046  stoweidlem57  46048  stoweidlem60  46051  stirlinglem5  46069  stirlinglem13  46077  stirlinglem14  46078  fourierdlem16  46114  fourierdlem20  46118  fourierdlem21  46119  fourierdlem22  46120  fourierdlem25  46123  fourierdlem31  46129  fourierdlem39  46137  fourierdlem41  46139  fourierdlem42  46140  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem77  46174  fourierdlem81  46178  fourierdlem83  46180  fourierdlem103  46200  fourierdlem104  46201  elaa2lem  46224  etransclem47  46272  qndenserrnbl  46286  ioorrnopnlem  46295  ioorrnopnxrlem  46297  intsaluni  46320  salgencntex  46334  subsaliuncllem  46348  sge0resplit  46397  sge0seq  46437  sge0reuz  46438  nnfoctbdjlem  46446  meaiininclem  46477  hoicvrrex  46547  ovnlecvr  46549  ovnlerp  46553  hoidmv1lelem2  46583  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  ovnlecvr2  46601  hoiqssbl  46616  ovolval4lem2  46641  ovolval5lem2  46644  ovnovollem1  46647  ovnovollem2  46648  iinhoiicclem  46664  smfinflem  46808  smflimsuplem7  46817  sprsymrelfolem2  47487  perfectALTV  47717  9gbo  47768  11gbo  47769  nnsum3primes4  47782  nnsum3primesprm  47784  ssnn0ssfz  48343  lincsumcl  48426  lincscmcl  48427  zlmodzxzldep  48499  ldepsnlinc  48503  line2ylem  48746  line2xlem  48748  sepfsepc  48922  lubsscl  48954  glbsscl  48955  nelsubc3lem  49065  cnelsubclem  49598  aacllem  49796