Theorem rspcev 3572

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057

This theorem is referenced by:  rspcedvdw  3575  rspceb2dv  3576  rspceaimv  3578  rspc2ev  3585  rspc3ev  3589  rspceeqv  3595  reu6i  3682  rspesbca  3827  eliuni  4945  iuneqconst  4951  brralrspcev  5149  wefrc  5608  wereu2  5611  xpdifid  6115  frpomin  6287  onfr  6345  onelssex  6355  ordunidif  6356  eliman0  6859  dffv2  6917  elrnrexdm  7022  eldmrexrn  7024  elabrex  7176  elabrexg  7177  f1elima  7197  fliftfun  7246  fliftval  7250  f1oiso2  7286  sorpssuni  7665  sorpssint  7666  onssmin  7725  onminex  7735  fimaproj  8065  frxp3  8081  poseq  8088  tfrlem12  8308  seqomlem2  8370  oawordeulem  8469  oaass  8476  odi  8494  omass  8495  omeulem1  8497  oen0  8501  oelim2  8510  oeeulem  8516  nnawordex  8552  nnaordex2  8554  eldifsucnn  8579  cofon1  8587  cofon2  8588  naddcllem  8591  naddunif  8608  boxcutc  8865  0fi  8964  snfi  8965  rexdif1en  9070  findcard  9073  nnfi  9077  pssnn  9078  unfi  9080  onfin  9124  dif1ennnALT  9161  frfi  9169  fisupg  9172  nnsdomg  9183  pwfir  9201  prfi  9208  fissuni  9241  fipreima  9242  finsschain  9243  indexfi  9244  marypha1lem  9317  eqsup  9340  supmax  9352  fisup2g  9353  fisupcl  9354  supisoex  9359  infmin  9380  fiinfg  9385  fiinf2g  9386  wofib  9431  wemaplem2  9433  card2inf  9441  brwdom2  9459  cnfcom3clem  9595  ssttrcl  9605  ttrcltr  9606  trcl  9618  frmin  9642  r1ordg  9671  r1pwss  9677  tz9.12lem3  9682  tz9.12  9683  r1elwf  9689  tcrank  9777  scottex  9778  scott0  9779  isnumi  9839  onsdom  9889  ondomen  9928  infpwfien  9953  cardaleph  9980  infenaleph  9982  alephfplem4  9998  alephfp2  10000  dfac2b  10022  ackbij1lem18  10127  ackbij1  10128  cflem  10136  cflemOLD  10137  cflecard  10144  cfsuc  10148  cfflb  10150  cofsmo  10160  coftr  10164  fin23lem7  10207  fin23lem11  10208  enfin2i  10212  fin23lem26  10216  isf32lem5  10248  isf34lem4  10268  isfin1-3  10277  fin1a2lem7  10297  axdc3lem4  10344  ttukeylem7  10406  iunfo  10430  ficard  10456  pwcfsdom  10474  fpwwe2lem11  10532  wunex  10630  eltsk2g  10642  grur1  10711  axgroth6  10719  inaprc  10727  nqereu  10820  archnq  10871  genpnmax  10898  ltexpri  10934  prlem936  10938  recexpr  10942  supexpr  10945  negexsr  10993  recexsrlem  10994  recexsr  10998  supsrlem  11002  axrnegex  11053  axrrecex  11054  axpre-sup  11060  1re  11112  dedekind  11276  dedekindle  11277  cnegex  11294  cnegex2  11295  recex  11749  receu  11762  fiminre2  12070  cju  12121  nn2ge  12152  nominpos  12358  zdiv  12543  btwnz  12576  uzwo  12809  ublbneg  12831  lbzbi  12834  zsupss  12835  uzsupss  12838  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem4  12878  rpnnen1lem5  12879  z2ge  13097  qbtwnre  13098  qbtwnxr  13099  xralrple  13104  xrsupsslem  13206  xrinfmsslem  13207  supxrpnf  13217  icc0  13293  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  18576  mgmidsssn0  18580  gsumval2a  18593  ismndd  18664  isgrpd2  18869  isgrpd  18871  imasgrp2  18968  mhmmnd  18977  ghmgrp  18979  gaorber  19220  orbsta  19225  cayleyth  19327  pmtrdifel  19392  pmtrdifwrdel  19397  pmtrdifwrdel2  19398  psgnunilem2  19407  psgnunilem3  19408  psgnvalii  19421  pgpfi1  19507  sylow1lem3  19512  sylow1lem5  19514  pgpfi  19517  sylow2alem2  19530  efgredeu  19664  lt6abl  19807  pgpfac1lem3a  19990  pgpfac1lem3  19991  pgpfac1lem5  19993  pgpfaclem1  19995  pgpfaclem3  19997  ablfaclem2  20000  dvdsrmul  20282  dvdsr01  20289  irredrmul  20345  rhmdvdsr  20423  rgspnval  20527  rgspncl  20528  lspf  20907  lspval  20908  lssats2  20933  lspfixed  21065  lspsolvlem  21079  zringlpir  21404  pzriprnglem13  21430  zncyg  21485  cygth  21508  frlmup4  21738  aspval  21810  evlseu  22018  fiinbas  22867  topbas  22887  pptbas  22923  clsval  22952  elcls  22988  neiint  23019  neips  23028  opnneissb  23029  opnssneib  23030  innei  23040  neiptopnei  23047  restbas  23073  neitr  23095  pnfnei  23135  mnfnei  23136  lmconst  23176  iscnp4  23178  cncnpi  23193  cnconst2  23198  cnprest  23204  cnpdis  23208  nrmsep  23272  regsep2  23291  cmpcovf  23306  cmpsub  23315  cmpcld  23317  hauscmplem  23321  conncompid  23346  2ndci  23363  2ndcsb  23364  2ndc1stc  23366  1stcrest  23368  2ndcctbss  23370  2ndcdisj  23371  2ndcomap  23373  2ndcsep  23374  dis2ndc  23375  restlly  23398  islly2  23399  hausllycmp  23409  cldllycmp  23410  lly1stc  23411  dislly  23412  ssref  23427  refref  23428  finlocfin  23435  dissnlocfin  23444  locfindis  23445  llycmpkgen2  23465  cmpkgen  23466  1stckgenlem  23468  elptr  23488  ptbasfi  23496  neitx  23522  ptpjopn  23527  txcnp  23535  ptcnplem  23536  txlly  23551  txnlly  23552  txtube  23555  txcmplem1  23556  tx1stc  23565  txkgen  23567  xkococnlem  23574  txconn  23604  tgqtop  23627  kqreglem1  23656  kqreglem2  23657  kqnrmlem1  23658  kqnrmlem2  23659  reghmph  23708  nrmhmph  23709  fbssfi  23752  opnfbas  23757  isfil2  23771  fsubbas  23782  ssfg  23787  fgss2  23789  fbasrn  23799  filuni  23800  fgtr  23805  ssufl  23833  uffix  23836  elfm2  23863  elfm3  23865  imaelfm  23866  rnelfmlem  23867  rnelfm  23868  fmfnfmlem4  23872  fmfnfm  23873  fmco  23876  ufldom  23877  hausflim  23896  flimcls  23900  hauspwpwf1  23902  flffbas  23910  txflf  23921  fclscf  23940  fclsfnflim  23942  alexsubALTlem4  23965  alexsubALT  23966  tmdgsum2  24011  symgtgp  24021  subgntr  24022  opnsubg  24023  ghmcnp  24030  qustgpopn  24035  tsmsfbas  24043  tsmsxplem1  24068  ustexsym  24131  trust  24144  utoptop  24149  restutop  24152  restutopopn  24153  ustuqtop4  24159  utopsnneiplem  24162  iducn  24197  fmucnd  24206  cfilufg  24207  trcfilu  24208  neipcfilu  24210  imasdsf1olem  24288  blssps  24339  blss  24340  blssexps  24341  blssex  24342  ssblex  24343  blin2  24344  neibl  24416  blcld  24420  metss2  24427  stdbdmopn  24433  met1stc  24436  met2ndci  24437  metrest  24439  prdsxmslem2  24444  metcnp3  24455  metustexhalf  24471  metustfbas  24472  cfilucfil  24474  restmetu  24485  dscopn  24488  ngptgp  24551  nlmvscnlem1  24601  tgioo  24711  tgqioo  24715  xrsmopn  24728  zcld  24729  recld2  24730  zdis  24732  icccmplem1  24738  icccmplem2  24739  xmetdcn2  24753  addcnlem  24780  xrhmeo  24871  cnheibor  24881  cnllycmp  24882  lebnumlem3  24889  lebnum  24890  xlebnum  24891  lebnumii  24892  elpi1i  24973  ipcnlem1  25172  lmnn  25190  iscfil3  25200  cfilres  25223  flimcfil  25241  bcthlem4  25254  bcthlem5  25255  minveclem4c  25352  minveclem2  25353  minveclem3b  25355  minveclem3  25356  minveclem4  25359  minveclem6  25361  ivthlem2  25380  ivth  25382  ivthle  25384  ivthle2  25385  elovolmr  25404  ovolunlem1  25425  ovoliunlem2  25431  ovolicc1  25444  iundisj  25476  iunmbl2  25485  dyadmbllem  25527  volivth  25535  mbflimsup  25594  i1faddlem  25621  i1fmullem  25622  itg2lr  25658  itg2monolem1  25678  limcnlp  25806  ellimc3  25807  limcflf  25809  limciun  25822  rollelem  25920  c1lip1  25929  lhop1lem  25945  ply1divex  26069  ig1peu  26107  elply2  26128  coeeq  26159  plydivlem3  26230  plydivlem4  26231  elqaalem3  26256  qaa  26258  iaa  26260  aareccl  26261  aannenlem2  26264  aalioulem2  26268  aalioulem3  26269  aalioulem5  26271  aalioulem6  26272  aaliou  26273  aaliou2  26275  aaliou3lem8  26280  ulmshftlem  26325  reeff1o  26384  pilem2  26389  pilem3  26390  efif1olem2  26479  efopn  26594  cxpcn3lem  26684  cxpeq  26694  dcubic2  26781  quart  26798  xrlimcnp  26905  ftalem5  27014  ftalem7  27016  sgmnncl  27084  dvdsppwf1o  27123  musum  27128  perfect  27169  dchrptlem1  27202  dchrptlem2  27203  dchrpt  27205  bpos1lem  27220  lgsqrlem4  27287  lgsdchrval  27292  2sqblem  27369  dchrisumlem3  27429  chpdifbndlem2  27492  pntrsumbnd2  27505  pntpbnd1  27524  pntpbnd2  27525  pntpbnd  27526  pntibndlem2  27529  pntibndlem3  27530  pntleme  27546  pntlem3  27547  elno2  27593  sltval2  27595  noreson  27599  sltres  27601  noseponlem  27603  nolesgn2o  27610  nogesgn1o  27612  nodense  27631  nosupfv  27645  nosupres  27646  nosupbnd1lem3  27649  nosupbnd1lem5  27651  nosupbnd2lem1  27654  noinffv  27660  noinfres  27661  noinfbnd1lem3  27664  noinfbnd1lem5  27666  noinfbnd2lem1  27669  noetasuplem4  27675  noetainflem4  27679  noetalem2  27681  cuteq0  27776  cuteq1  27778  oldlim  27832  bdayiun  27860  cofcutrtime  27871  cofss  27874  coiniss  27875  cutlt  27876  cutmax  27878  cutmin  27879  negsex  27985  negsfo  27995  norecdiv  28129  divs1  28143  precsexlem11  28155  precsex  28156  recsex  28157  elons2d  28196  onscutlt  28201  n0ons  28264  bdayn0sf1o  28295  dfnns2  28297  zsoring  28332  pw2recs  28361  halfcut  28378  0reno  28399  readdscl  28401  axtgcont  28447  tgcgrxfr  28496  legid  28565  btwnleg  28566  leg0  28570  tghilberti1  28615  tglnpt2  28619  colline  28627  mirreu3  28632  isperp2  28693  colperpex  28711  lnopp2hpgb  28741  hpgerlem  28743  brbtwn  28877  brcgr  28878  brbtwn2  28883  axpasch  28919  axlowdimlem14  28933  axlowdim2  28938  axcontlem2  28943  axcontlem4  28945  axcontlem8  28949  axcontlem10  28951  axcontlem12  28953  fusgrn0degnn0  29478  friendshipgt3  30378  lpni  30460  isgrpoi  30478  vacn  30674  smcnlem  30677  nmosetn0  30745  nmoolb  30751  nmobndi  30755  nmoo0  30771  nmlno0lem  30773  isblo3i  30781  blo3i  30782  blocnilem  30784  ubthlem1  30850  minvecolem2  30855  minvecolem3  30856  minvecolem4c  30859  minvecolem4  30860  minvecolem5  30861  minvecolem6  30862  norm1exi  31230  occl  31284  spanval  31313  spancl  31316  shsval2i  31367  ococin  31388  pjoml6i  31569  nmopsetn0  31845  nmfnsetn0  31858  nmoplb  31887  nmfnlb  31904  nmop0  31966  nmfn0  31967  nmlnop0iALT  31975  nmopun  31994  nmcexi  32006  lnconi  32013  lnopcnbd  32016  lnfncnbd  32037  riesz3i  32042  riesz1  32045  cnlnadjlem2  32048  cnlnadjlem8  32054  cnlnadjlem9  32055  adjbd1o  32065  branmfn  32085  opsqrlem1  32120  pjnmopi  32128  strlem1  32230  stri  32237  hstri  32245  cvcon3  32264  cvnbtwn  32266  superpos  32334  shatomici  32338  atcvat4i  32377  mdsymlem2  32384  cdj1i  32413  cdj3i  32421  rexunirn  32471  foresf1o  32484  iundisjf  32569  aciunf1lem  32644  fnpreimac  32653  fgreu  32654  fcnvgreu  32655  xrge0infss  32743  ssnnssfz  32770  iundisjfi  32778  indf1ofs  32847  xreceu  32902  rexdiv  32906  isarchi3  33156  archirngz  33158  archiabllem2a  33163  0nellinds  33335  qtophaus  33849  reff  33852  locfinreflem  33853  cmpcref  33863  dispcmp  33872  tpr2rico  33925  pnfneige0  33964  qqhucn  34005  rrhre  34034  esumcst  34076  esumpcvgval  34091  dmsigagen  34157  rossros  34193  dya2icoseg  34290  dya2iocnrect  34294  dya2iocuni  34296  eulerpartlemgvv  34389  dstfrvunirn  34488  ballotlem4  34512  ballotlemic  34520  ballotlem1c  34521  ballotlemrc  34544  signsw0g  34569  signswmnd  34570  prodfzo03  34616  tgoldbachgt  34676  onvf1odlem4  35150  loop1cycl  35181  umgr2cycllem  35184  umgr2cycl  35185  subfacp1lem3  35226  erdsze2lem2  35248  cnpconn  35274  txpconn  35276  ptpconn  35277  indispconn  35278  connpconn  35279  cvxpconn  35286  cnllysconn  35289  cvmsss2  35318  cvmcov2  35319  cvmopnlem  35322  cvmliftlem14  35341  cvmliftlem15  35342  cvmlift2lem11  35357  cvmlift2lem12  35358  cvmlift2lem13  35359  cvmlift3lem2  35364  cvmlift3lem6  35368  cvmlift3lem9  35371  mthmi  35621  r1peuqusdeg1  35687  br8  35800  br6  35801  br4  35802  dfon2lem9  35833  wzel  35866  wsuclem  35867  wsuclb  35870  imagesset  35997  fvtransport  36076  brcolinear  36103  brsegle  36152  seglerflx  36156  seglemin  36157  btwnsegle  36161  fvray  36185  fvline  36188  hilbert1.1  36198  elhf2  36219  0hf  36221  nn0prpwlem  36366  nn0prpw  36367  fness  36393  fneref  36394  fnessref  36401  refssfne  36402  neibastop2lem  36404  fnemeet1  36410  tailfb  36421  filnetlem4  36425  limsucncmpi  36489  taupilemrplb  37364  relowlssretop  37407  rdgellim  37420  matunitlindflem2  37667  ptrecube  37670  poimirlem4  37674  poimirlem17  37687  poimirlem20  37690  poimirlem23  37693  poimirlem24  37694  poimirlem26  37696  poimirlem27  37697  poimirlem29  37699  poimirlem32  37702  heicant  37705  mblfinlem1  37707  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  volsupnfl  37715  itg2addnclem  37721  itg2addnclem3  37723  itg2addnc  37724  ftc1anclem5  37747  unirep  37764  cover2  37765  indexa  37783  frinfm  37785  sdclem1  37793  fdc  37795  incsequz  37798  caushft  37811  istotbnd3  37821  0totbnd  37823  sstotbnd2  37824  sstotbnd  37825  sstotbnd3  37826  isbnd3  37834  ssbnd  37838  equivbnd  37840  prdsbnd  37843  prdstotbnd  37844  cntotbnd  37846  heibor1lem  37859  heiborlem1  37861  heiborlem3  37863  heiborlem6  37866  heiborlem8  37868  bfplem2  37873  rrncmslem  37882  iccbnd  37890  opidonOLD  37902  exidres  37928  isrngod  37948  isgrpda  38005  isdrngo2  38008  igenval  38111  igenidl  38113  prtlem10  38974  lshpnel2N  39094  lsmsat  39117  lssatomic  39120  lcvnbtwn  39134  lfl1  39179  eqlkr  39208  lshpkrlem1  39219  lshpkrex  39227  cvrcon3b  39386  cvrat4  39552  3dim3  39578  ps-2  39587  llni  39617  llnle  39627  lplni  39641  lplnle  39649  lplnexllnN  39673  lvoli  39684  lnatexN  39888  elpaddn0  39909  pclfinN  40009  lhprelat3N  40149  4atexlemex2  40180  4atex  40185  4atex2-0aOLDN  40187  4atex2-0cOLDN  40189  lautcvr  40201  cdleme0ex1N  40332  cdleme50rnlem  40653  cdleme50ex  40668  cdlemg1cex  40697  cdlemkid5  41044  cdlemk  41083  tendoex  41084  cdleml5N  41089  cdlemm10N  41227  dih1dimatlem0  41437  dihjat1lem  41537  dvh3dim2  41557  dvh3dim3N  41558  dochkr1  41587  dochkr1OLDN  41588  lcfrvalsnN  41650  lcfrlem27  41678  lcfrlem37  41688  lcfr  41694  mapd1o  41757  mapdpglem23  41803  hdmap11lem2  41951  primrootsunit1  42200  zdivgd  42440  resubeu  42480  fidomncyc  42638  nacsfix  42815  mzpcompact2lem  42854  eldioph  42861  diophrw  42862  diophin  42875  rexrabdioph  42897  rexzrexnn0  42907  eldioph4b  42914  rencldnfilem  42923  irrapxlem5  42929  irrapxlem6  42930  pell1234qrdich  42964  pell14qrdich  42972  infmrgelbi  42981  pellqrex  42982  pellfundre  42984  pellfundlb  42987  rmxynorm  43021  congrep  43076  acongrep  43083  jm2.27  43111  fnwe2lem2  43154  islssfgi  43175  hbtlem2  43227  hbtlem4  43229  hbtlem5  43231  dgraaub  43251  mpaaeu  43253  aaitgo  43265  unielss  43321  onexgt  43343  onexomgt  43344  onexlimgt  43346  onexoegt  43347  oaordnr  43399  omnord1  43408  oenord1  43419  oaomoencom  43420  oenass  43422  tfsconcatfv2  43443  tfsconcatrn  43445  tfsconcatb0  43447  ofoafo  43459  naddcnffo  43467  oaun3lem1  43477  naddwordnexlem4  43504  sucomisnotcard  43647  clsk1independent  44149  0elaxnul  45086  pwclaxpow  45087  prclaxpr  45088  uniclaxun  45089  omssaxinf2  45091  wfac8prim  45105  restuni3  45225  iinssd  45238  founiiun  45286  wessf1ornlem  45292  founiiun0  45297  unirnmap  45315  dstregt0  45393  uzfissfz  45435  rpgtrecnn  45488  rexabslelem  45526  infrnmptle  45531  infxrunb3rnmpt  45536  infxrpnf  45554  supminfxr  45572  rexanuz2nf  45600  iooiinicc  45652  iooiinioc  45666  uzubioo  45675  climsuse  45718  islptre  45729  limsuppnfdlem  45809  climinf3  45824  limsupmnfuzlem  45834  limsupre3lem  45840  limsupre3uzlem  45843  0cnv  45850  liminfreuzlem  45910  cnrefiisplem  45937  icccncfext  45995  cncficcgt0  45996  dvbdfbdioo  46038  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  stoweidlem9  46117  stoweidlem14  46122  stoweidlem18  46126  stoweidlem21  46129  stoweidlem29  46137  stoweidlem34  46142  stoweidlem35  46143  stoweidlem39  46147  stoweidlem41  46149  stoweidlem45  46153  stoweidlem52  46160  stoweidlem55  46163  stoweidlem57  46165  stoweidlem60  46168  stirlinglem5  46186  stirlinglem13  46194  stirlinglem14  46195  fourierdlem16  46231  fourierdlem20  46235  fourierdlem21  46236  fourierdlem22  46237  fourierdlem25  46240  fourierdlem31  46246  fourierdlem39  46254  fourierdlem41  46256  fourierdlem42  46257  fourierdlem47  46261  fourierdlem48  46262  fourierdlem49  46263  fourierdlem51  46265  fourierdlem63  46277  fourierdlem64  46278  fourierdlem65  46279  fourierdlem77  46291  fourierdlem81  46295  fourierdlem83  46297  fourierdlem103  46317  fourierdlem104  46318  elaa2lem  46341  etransclem47  46389  qndenserrnbl  46403  ioorrnopnlem  46412  ioorrnopnxrlem  46414  intsaluni  46437  salgencntex  46451  subsaliuncllem  46465  sge0resplit  46514  sge0seq  46554  sge0reuz  46555  nnfoctbdjlem  46563  meaiininclem  46594  hoicvrrex  46664  ovnlecvr  46666  ovnlerp  46670  hoidmv1lelem2  46700  hoidmvlelem2  46704  hoidmvlelem3  46705  ovnhoilem1  46709  ovnlecvr2  46718  hoiqssbl  46733  ovolval4lem2  46758  ovolval5lem2  46761  ovnovollem1  46764  ovnovollem2  46765  iinhoiicclem  46781  smfinflem  46925  smflimsuplem7  46934  nthrucw  46994  sprsymrelfolem2  47603  perfectALTV  47833  9gbo  47884  11gbo  47885  nnsum3primes4  47898  nnsum3primesprm  47900  ssnn0ssfz  48459  lincsumcl  48542  lincscmcl  48543  zlmodzxzldep  48615  ldepsnlinc  48619  line2ylem  48862  line2xlem  48864  sepfsepc  49038  lubsscl  49070  glbsscl  49071  nelsubc3lem  49181  cnelsubclem  49714  aacllem  49912