Theorem rspcev 3565

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  rspcedvdw  3568  rspceaimv  3571  rspc2ev  3578  rspc3ev  3582  rspceeqv  3588  reu6i  3675  rspesbca  3820  eliuni  4940  iuneqconst  4946  brralrspcev  5146  wefrc  5619  wereu2  5622  xpdifid  6127  frpomin  6299  onfr  6357  onelssex  6367  ordunidif  6368  eliman0  6872  dffv2  6930  elrnrexdm  7036  eldmrexrn  7038  elabrex  7191  elabrexg  7192  f1elima  7212  fliftfun  7261  fliftval  7265  f1oiso2  7301  sorpssuni  7680  sorpssint  7681  onssmin  7740  onminex  7750  fimaproj  8079  frxp3  8095  poseq  8102  tfrlem12  8322  seqomlem2  8384  oawordeulem  8483  oaass  8490  odi  8508  omass  8509  omeulem1  8511  oen0  8516  oelim2  8525  oeeulem  8531  nnawordex  8567  nnaordex2  8569  eldifsucnn  8594  cofon1  8602  cofon2  8603  naddcllem  8606  naddunif  8623  boxcutc  8883  0fi  8983  snfi  8984  rexdif1en  9089  findcard  9092  nnfi  9096  pssnn  9097  unfi  9099  onfin  9143  dif1ennnALT  9181  frfi  9189  fisupg  9192  nnsdomg  9203  pwfir  9221  prfi  9228  fissuni  9261  fipreima  9262  finsschain  9263  indexfi  9264  marypha1lem  9340  eqsup  9363  supmax  9375  fisup2g  9376  fisupcl  9377  supisoex  9382  infmin  9403  fiinfg  9408  fiinf2g  9409  wofib  9454  wemaplem2  9456  card2inf  9464  brwdom2  9482  cnfcom3clem  9620  ssttrcl  9630  ttrcltr  9631  trcl  9643  frmin  9667  r1ordg  9696  r1pwss  9702  tz9.12lem3  9707  tz9.12  9708  r1elwf  9714  tcrank  9802  scottex  9803  scott0  9804  isnumi  9864  onsdom  9914  ondomen  9953  infpwfien  9978  cardaleph  10005  infenaleph  10007  alephfplem4  10023  alephfp2  10025  dfac2b  10047  ackbij1lem18  10152  ackbij1  10153  cflem  10161  cflemOLD  10162  cflecard  10169  cfsuc  10173  cfflb  10175  cofsmo  10185  coftr  10189  fin23lem7  10232  fin23lem11  10233  enfin2i  10237  fin23lem26  10241  isf32lem5  10273  isf34lem4  10293  isfin1-3  10302  fin1a2lem7  10322  axdc3lem4  10369  ttukeylem7  10431  iunfo  10455  ficard  10481  pwcfsdom  10500  fpwwe2lem11  10558  wunex  10656  eltsk2g  10668  grur1  10737  axgroth6  10745  inaprc  10753  nqereu  10846  archnq  10897  genpnmax  10924  ltexpri  10960  prlem936  10964  recexpr  10968  supexpr  10971  negexsr  11019  recexsrlem  11020  recexsr  11024  supsrlem  11028  axrnegex  11079  axrrecex  11080  axpre-sup  11086  1re  11138  dedekind  11303  dedekindle  11304  cnegex  11321  cnegex2  11322  recex  11776  receu  11789  fiminre2  12098  cju  12149  nn2ge  12198  nominpos  12408  zdiv  12593  btwnz  12626  uzwo  12855  ublbneg  12877  lbzbi  12880  zsupss  12881  uzsupss  12884  rpnnen1lem1  12922  rpnnen1lem3  12923  rpnnen1lem4  12924  rpnnen1lem5  12925  z2ge  13144  qbtwnre  13145  qbtwnxr  13146  xralrple  13151  xrsupsslem  13253  xrinfmsslem  13254  supxrpnf  13264  icc0  13340  uzsup  13816  expnbnd  14188  expmulnbnd  14191  hashkf  14288  hashdom  14335  iswrdi  14473  rtrclreclem1  15013  rtrclreclem2  15015  rtrclreclem3  15016  01sqrex  15205  resqrex  15206  sqrtneg  15223  abs1m  15292  rexanuz  15302  rexuz3  15305  rexuzre  15309  sqreu  15317  o1lo1  15493  climconst  15499  rlimclim1  15501  climshftlem  15530  rlimo1  15573  lo1add  15583  lo1mul  15584  lo1le  15608  isercoll  15624  serf0  15637  zsum  15674  fsum  15676  fsumcvg3  15685  mertenslem1  15843  ntrivcvgn0  15857  ntrivcvgmullem  15860  zprod  15896  fprod  15900  fprodntriv  15901  dvdsval2  16218  dvds0lem  16229  dvds1lem  16230  dvds2lem  16231  odd2np1lem  16303  odd2np1  16304  opeo  16328  omeo  16329  divalglem9  16364  gcdcllem3  16464  lcmcllem  16559  qredeu  16621  exprmfct  16668  isprm5  16671  odzcllem  16757  reumodprminv  16769  modprm0  16770  nnnn0modprm0  16771  pythagtriplem19  16798  pcprmpw2  16847  pockthi  16872  infpnlem2  16876  vdwlem2  16947  vdwlem10  16955  vdwlem13  16958  ramub1lem1  16991  cshwrepswhash1  17067  imasleval  17499  mreexexlem3d  17606  mreexexlem4d  17607  iscatd  17633  cat1  18058  poslubd  18371  fpwipodrs  18500  ismgmid2  18630  mgmidsssn0  18634  gsumval2a  18647  ismndd  18718  isgrpd2  18926  isgrpd  18928  imasgrp2  19025  mhmmnd  19034  ghmgrp  19036  gaorber  19277  orbsta  19282  cayleyth  19384  pmtrdifel  19449  pmtrdifwrdel  19454  pmtrdifwrdel2  19455  psgnunilem2  19464  psgnunilem3  19465  psgnvalii  19478  pgpfi1  19564  sylow1lem3  19569  sylow1lem5  19571  pgpfi  19574  sylow2alem2  19587  efgredeu  19721  lt6abl  19864  pgpfac1lem3a  20047  pgpfac1lem3  20048  pgpfac1lem5  20050  pgpfaclem1  20052  pgpfaclem3  20054  ablfaclem2  20057  dvdsrmul  20338  dvdsr01  20345  irredrmul  20401  rhmdvdsr  20479  rgspnval  20583  rgspncl  20584  lspf  20963  lspval  20964  lssats2  20989  lspfixed  21121  lspsolvlem  21135  zringlpir  21460  pzriprnglem13  21486  zncyg  21541  cygth  21564  frlmup4  21794  aspval  21865  evlseu  22074  fiinbas  22930  topbas  22950  pptbas  22986  clsval  23015  elcls  23051  neiint  23082  neips  23091  opnneissb  23092  opnssneib  23093  innei  23103  neiptopnei  23110  restbas  23136  neitr  23158  pnfnei  23198  mnfnei  23199  lmconst  23239  iscnp4  23241  cncnpi  23256  cnconst2  23261  cnprest  23267  cnpdis  23271  nrmsep  23335  regsep2  23354  cmpcovf  23369  cmpsub  23378  cmpcld  23380  hauscmplem  23384  conncompid  23409  2ndci  23426  2ndcsb  23427  2ndc1stc  23429  1stcrest  23431  2ndcctbss  23433  2ndcdisj  23434  2ndcomap  23436  2ndcsep  23437  dis2ndc  23438  restlly  23461  islly2  23462  hausllycmp  23472  cldllycmp  23473  lly1stc  23474  dislly  23475  ssref  23490  refref  23491  finlocfin  23498  dissnlocfin  23507  locfindis  23508  llycmpkgen2  23528  cmpkgen  23529  1stckgenlem  23531  elptr  23551  ptbasfi  23559  neitx  23585  ptpjopn  23590  txcnp  23598  ptcnplem  23599  txlly  23614  txnlly  23615  txtube  23618  txcmplem1  23619  tx1stc  23628  txkgen  23630  xkococnlem  23637  txconn  23667  tgqtop  23690  kqreglem1  23719  kqreglem2  23720  kqnrmlem1  23721  kqnrmlem2  23722  reghmph  23771  nrmhmph  23772  fbssfi  23815  opnfbas  23820  isfil2  23834  fsubbas  23845  ssfg  23850  fgss2  23852  fbasrn  23862  filuni  23863  fgtr  23868  ssufl  23896  uffix  23899  elfm2  23926  elfm3  23928  imaelfm  23929  rnelfmlem  23930  rnelfm  23931  fmfnfmlem4  23935  fmfnfm  23936  fmco  23939  ufldom  23940  hausflim  23959  flimcls  23963  hauspwpwf1  23965  flffbas  23973  txflf  23984  fclscf  24003  fclsfnflim  24005  alexsubALTlem4  24028  alexsubALT  24029  tmdgsum2  24074  symgtgp  24084  subgntr  24085  opnsubg  24086  ghmcnp  24093  qustgpopn  24098  tsmsfbas  24106  tsmsxplem1  24131  ustexsym  24194  trust  24207  utoptop  24212  restutop  24215  restutopopn  24216  ustuqtop4  24222  utopsnneiplem  24225  iducn  24260  fmucnd  24269  cfilufg  24270  trcfilu  24271  neipcfilu  24273  imasdsf1olem  24351  blssps  24402  blss  24403  blssexps  24404  blssex  24405  ssblex  24406  blin2  24407  neibl  24479  blcld  24483  metss2  24490  stdbdmopn  24496  met1stc  24499  met2ndci  24500  metrest  24502  prdsxmslem2  24507  metcnp3  24518  metustexhalf  24534  metustfbas  24535  cfilucfil  24537  restmetu  24548  dscopn  24551  ngptgp  24614  nlmvscnlem1  24664  tgioo  24774  tgqioo  24778  xrsmopn  24791  zcld  24792  recld2  24793  zdis  24795  icccmplem1  24801  icccmplem2  24802  xmetdcn2  24816  addcnlem  24843  xrhmeo  24926  cnheibor  24935  cnllycmp  24936  lebnumlem3  24943  lebnum  24944  xlebnum  24945  lebnumii  24946  elpi1i  25026  ipcnlem1  25225  lmnn  25243  iscfil3  25253  cfilres  25276  flimcfil  25294  bcthlem4  25307  bcthlem5  25308  minveclem4c  25405  minveclem2  25406  minveclem3b  25408  minveclem3  25409  minveclem4  25412  minveclem6  25414  ivthlem2  25432  ivth  25434  ivthle  25436  ivthle2  25437  elovolmr  25456  ovolunlem1  25477  ovoliunlem2  25483  ovolicc1  25496  iundisj  25528  iunmbl2  25537  dyadmbllem  25579  volivth  25587  mbflimsup  25646  i1faddlem  25673  i1fmullem  25674  itg2lr  25710  itg2monolem1  25730  limcnlp  25858  ellimc3  25859  limcflf  25861  limciun  25874  rollelem  25969  c1lip1  25977  lhop1lem  25993  ply1divex  26115  ig1peu  26153  elply2  26174  coeeq  26205  plydivlem3  26275  plydivlem4  26276  elqaalem3  26301  qaa  26303  iaa  26305  aareccl  26306  aannenlem2  26309  aalioulem2  26313  aalioulem3  26314  aalioulem5  26316  aalioulem6  26317  aaliou  26318  aaliou2  26320  aaliou3lem8  26325  ulmshftlem  26370  reeff1o  26428  pilem2  26433  pilem3  26434  efif1olem2  26523  efopn  26638  cxpcn3lem  26727  cxpeq  26737  dcubic2  26824  quart  26841  xrlimcnp  26948  ftalem5  27057  ftalem7  27059  sgmnncl  27127  dvdsppwf1o  27166  musum  27171  perfect  27211  dchrptlem1  27244  dchrptlem2  27245  dchrpt  27247  bpos1lem  27262  lgsqrlem4  27329  lgsdchrval  27334  2sqblem  27411  dchrisumlem3  27471  chpdifbndlem2  27534  pntrsumbnd2  27547  pntpbnd1  27566  pntpbnd2  27567  pntpbnd  27568  pntibndlem2  27571  pntibndlem3  27572  pntleme  27588  pntlem3  27589  elno2  27635  ltsval2  27637  noreson  27641  ltsres  27643  noseponlem  27645  nolesgn2o  27652  nogesgn1o  27654  nodense  27673  nosupfv  27687  nosupres  27688  nosupbnd1lem3  27691  nosupbnd1lem5  27693  nosupbnd2lem1  27696  noinffv  27702  noinfres  27703  noinfbnd1lem3  27706  noinfbnd1lem5  27708  noinfbnd2lem1  27711  noetasuplem4  27717  noetainflem4  27721  noetalem2  27723  cuteq0  27824  cuteq1  27826  oldlim  27896  bdayiun  27924  cofcutrtime  27936  cofss  27939  coiniss  27940  cutlt  27941  cutmax  27943  cutmin  27944  negsex  28052  negsfo  28062  norecdiv  28199  divs1  28213  precsexlem11  28226  precsex  28227  recsex  28228  elons2d  28268  oncutlt  28273  n0on  28345  bdayn0sf1o  28379  dfnns2  28381  zsoring  28418  pw2recs  28447  halfcut  28467  0reno  28505  1reno  28506  readdscl  28508  axtgcont  28554  tgcgrxfr  28603  legid  28672  btwnleg  28673  leg0  28677  tghilberti1  28722  tglnpt2  28726  colline  28734  mirreu3  28739  isperp2  28800  colperpex  28818  lnopp2hpgb  28848  hpgerlem  28850  brbtwn  28985  brcgr  28986  brbtwn2  28991  axpasch  29027  axlowdimlem14  29041  axlowdim2  29046  axcontlem2  29051  axcontlem4  29053  axcontlem8  29057  axcontlem10  29059  axcontlem12  29061  fusgrn0degnn0  29586  friendshipgt3  30486  lpni  30569  isgrpoi  30587  vacn  30783  smcnlem  30786  nmosetn0  30854  nmoolb  30860  nmobndi  30864  nmoo0  30880  nmlno0lem  30882  isblo3i  30890  blo3i  30891  blocnilem  30893  ubthlem1  30959  minvecolem2  30964  minvecolem3  30965  minvecolem4c  30968  minvecolem4  30969  minvecolem5  30970  minvecolem6  30971  norm1exi  31339  occl  31393  spanval  31422  spancl  31425  shsval2i  31476  ococin  31497  pjoml6i  31678  nmopsetn0  31954  nmfnsetn0  31967  nmoplb  31996  nmfnlb  32013  nmop0  32075  nmfn0  32076  nmlnop0iALT  32084  nmopun  32103  nmcexi  32115  lnconi  32122  lnopcnbd  32125  lnfncnbd  32146  riesz3i  32151  riesz1  32154  cnlnadjlem2  32157  cnlnadjlem8  32163  cnlnadjlem9  32164  adjbd1o  32174  branmfn  32194  opsqrlem1  32229  pjnmopi  32237  strlem1  32339  stri  32346  hstri  32354  cvcon3  32373  cvnbtwn  32375  superpos  32443  shatomici  32447  atcvat4i  32486  mdsymlem2  32493  cdj1i  32522  cdj3i  32530  rexunirn  32579  foresf1o  32592  iundisjf  32677  aciunf1lem  32753  fnpreimac  32761  fgreu  32762  fcnvgreu  32763  xrge0infss  32851  ssnnssfz  32878  iundisjfi  32887  indf1ofs  32944  xreceu  32999  rexdiv  33003  isarchi3  33266  archirngz  33268  archiabllem2a  33273  0nellinds  33448  qtophaus  33999  reff  34002  locfinreflem  34003  cmpcref  34013  dispcmp  34022  tpr2rico  34075  pnfneige0  34114  qqhucn  34155  rrhre  34184  esumcst  34226  esumpcvgval  34241  dmsigagen  34307  rossros  34343  dya2icoseg  34440  dya2iocnrect  34444  dya2iocuni  34446  eulerpartlemgvv  34539  dstfrvunirn  34638  ballotlem4  34662  ballotlemic  34670  ballotlem1c  34671  ballotlemrc  34694  signsw0g  34719  signswmnd  34720  prodfzo03  34766  tgoldbachgt  34826  onvf1odlem4  35307  loop1cycl  35338  umgr2cycllem  35341  umgr2cycl  35342  subfacp1lem3  35383  erdsze2lem2  35405  cnpconn  35431  txpconn  35433  ptpconn  35434  indispconn  35435  connpconn  35436  cvxpconn  35443  cnllysconn  35446  cvmsss2  35475  cvmcov2  35476  cvmopnlem  35479  cvmliftlem14  35498  cvmliftlem15  35499  cvmlift2lem11  35514  cvmlift2lem12  35515  cvmlift2lem13  35516  cvmlift3lem2  35521  cvmlift3lem6  35525  cvmlift3lem9  35528  mthmi  35778  r1peuqusdeg1  35844  br8  35957  br6  35958  br4  35959  dfon2lem9  35990  wzel  36023  wsuclem  36024  wsuclb  36027  imagesset  36154  fvtransport  36233  brcolinear  36260  brsegle  36309  seglerflx  36313  seglemin  36314  btwnsegle  36318  fvray  36342  fvline  36345  hilbert1.1  36355  elhf2  36376  0hf  36378  nn0prpwlem  36523  nn0prpw  36524  fness  36550  fneref  36551  fnessref  36558  refssfne  36559  neibastop2lem  36561  fnemeet1  36567  tailfb  36578  filnetlem4  36582  limsucncmpi  36646  ttctr  36694  dfttc2g  36707  taupilemrplb  37653  relowlssretop  37696  rdgellim  37709  matunitlindflem2  37955  ptrecube  37958  poimirlem4  37962  poimirlem17  37975  poimirlem20  37978  poimirlem23  37981  poimirlem24  37982  poimirlem26  37984  poimirlem27  37985  poimirlem29  37987  poimirlem32  37990  heicant  37993  mblfinlem1  37995  mblfinlem2  37996  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  volsupnfl  38003  itg2addnclem  38009  itg2addnclem3  38011  itg2addnc  38012  ftc1anclem5  38035  unirep  38052  cover2  38053  indexa  38071  frinfm  38073  sdclem1  38081  fdc  38083  incsequz  38086  caushft  38099  istotbnd3  38109  0totbnd  38111  sstotbnd2  38112  sstotbnd  38113  sstotbnd3  38114  isbnd3  38122  ssbnd  38126  equivbnd  38128  prdsbnd  38131  prdstotbnd  38132  cntotbnd  38134  heibor1lem  38147  heiborlem1  38149  heiborlem3  38151  heiborlem6  38154  heiborlem8  38156  bfplem2  38161  rrncmslem  38170  iccbnd  38178  opidonOLD  38190  exidres  38216  isrngod  38236  isgrpda  38293  isdrngo2  38296  igenval  38399  igenidl  38401  prtlem10  39328  lshpnel2N  39448  lsmsat  39471  lssatomic  39474  lcvnbtwn  39488  lfl1  39533  eqlkr  39562  lshpkrlem1  39573  lshpkrex  39581  cvrcon3b  39740  cvrat4  39906  3dim3  39932  ps-2  39941  llni  39971  llnle  39981  lplni  39995  lplnle  40003  lplnexllnN  40027  lvoli  40038  lnatexN  40242  elpaddn0  40263  pclfinN  40363  lhprelat3N  40503  4atexlemex2  40534  4atex  40539  4atex2-0aOLDN  40541  4atex2-0cOLDN  40543  lautcvr  40555  cdleme0ex1N  40686  cdleme50rnlem  41007  cdleme50ex  41022  cdlemg1cex  41051  cdlemkid5  41398  cdlemk  41437  tendoex  41438  cdleml5N  41443  cdlemm10N  41581  dih1dimatlem0  41791  dihjat1lem  41891  dvh3dim2  41911  dvh3dim3N  41912  dochkr1  41941  dochkr1OLDN  41942  lcfrvalsnN  42004  lcfrlem27  42032  lcfrlem37  42042  lcfr  42048  mapd1o  42111  mapdpglem23  42157  hdmap11lem2  42305  primrootsunit1  42553  zdivgd  42786  resubeu  42826  fidomncyc  42997  nacsfix  43161  mzpcompact2lem  43200  eldioph  43207  diophrw  43208  diophin  43221  rexrabdioph  43243  rexzrexnn0  43253  eldioph4b  43260  rencldnfilem  43269  irrapxlem5  43275  irrapxlem6  43276  pell1234qrdich  43310  pell14qrdich  43318  infmrgelbi  43327  pellqrex  43328  pellfundre  43330  pellfundlb  43333  rmxynorm  43367  congrep  43422  acongrep  43429  jm2.27  43457  fnwe2lem2  43500  islssfgi  43521  hbtlem2  43573  hbtlem4  43575  hbtlem5  43577  dgraaub  43597  mpaaeu  43599  aaitgo  43611  unielss  43667  onexgt  43689  onexomgt  43690  onexlimgt  43692  onexoegt  43693  oaordnr  43745  omnord1  43754  oenord1  43765  oaomoencom  43766  oenass  43768  tfsconcatfv2  43789  tfsconcatrn  43791  tfsconcatb0  43793  ofoafo  43805  naddcnffo  43813  oaun3lem1  43823  naddwordnexlem4  43850  sucomisnotcard  43992  clsk1independent  44494  0elaxnul  45431  pwclaxpow  45432  prclaxpr  45433  uniclaxun  45434  omssaxinf2  45436  wfac8prim  45450  restuni3  45569  iinssd  45582  founiiun  45630  wessf1ornlem  45636  founiiun0  45641  unirnmap  45658  dstregt0  45736  uzfissfz  45777  rpgtrecnn  45830  rexabslelem  45867  infrnmptle  45872  infxrunb3rnmpt  45877  infxrpnf  45895  supminfxr  45913  rexanuz2nf  45941  iooiinicc  45993  iooiinioc  46007  uzubioo  46016  climsuse  46059  islptre  46070  limsuppnfdlem  46150  climinf3  46165  limsupmnfuzlem  46175  limsupre3lem  46181  limsupre3uzlem  46184  0cnv  46191  liminfreuzlem  46251  cnrefiisplem  46278  icccncfext  46336  cncficcgt0  46337  dvbdfbdioo  46379  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  stoweidlem9  46458  stoweidlem14  46463  stoweidlem18  46467  stoweidlem21  46470  stoweidlem29  46478  stoweidlem34  46483  stoweidlem35  46484  stoweidlem39  46488  stoweidlem41  46490  stoweidlem45  46494  stoweidlem52  46501  stoweidlem55  46504  stoweidlem57  46506  stoweidlem60  46509  stirlinglem5  46527  stirlinglem13  46535  stirlinglem14  46536  fourierdlem16  46572  fourierdlem20  46576  fourierdlem21  46577  fourierdlem22  46578  fourierdlem25  46581  fourierdlem31  46587  fourierdlem39  46595  fourierdlem41  46597  fourierdlem42  46598  fourierdlem47  46602  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem77  46632  fourierdlem81  46636  fourierdlem83  46638  fourierdlem103  46658  fourierdlem104  46659  elaa2lem  46682  etransclem47  46730  qndenserrnbl  46744  ioorrnopnlem  46753  ioorrnopnxrlem  46755  intsaluni  46778  salgencntex  46792  subsaliuncllem  46806  sge0resplit  46855  sge0seq  46895  sge0reuz  46896  nnfoctbdjlem  46904  meaiininclem  46935  hoicvrrex  47005  ovnlecvr  47007  ovnlerp  47011  hoidmv1lelem2  47041  hoidmvlelem2  47045  hoidmvlelem3  47046  ovnhoilem1  47050  ovnlecvr2  47059  hoiqssbl  47074  ovolval4lem2  47099  ovolval5lem2  47102  ovnovollem1  47105  ovnovollem2  47106  iinhoiicclem  47122  smfinflem  47266  smflimsuplem7  47275  nthrucw  47335  sprsymrelfolem2  47968  perfectALTV  48214  9gbo  48265  11gbo  48266  nnsum3primes4  48279  nnsum3primesprm  48281  ssnn0ssfz  48840  lincsumcl  48922  lincscmcl  48923  zlmodzxzldep  48995  ldepsnlinc  48999  line2ylem  49242  line2xlem  49244  sepfsepc  49418  lubsscl  49450  glbsscl  49451  nelsubc3lem  49560  cnelsubclem  50093  aacllem  50291