Theorem rspcev 3588

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 3581	. 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  3591  rspceb2dv  3592  rspceaimv  3594  rspc2ev  3601  rspc3ev  3605  rspceeqv  3611  reu6i  3699  rspesbca  3844  eliuni  4961  iuneqconst  4967  brralrspcev  5167  wefrc  5632  wereu2  5635  xpdifid  6141  frpomin  6313  onfr  6371  onelssex  6381  ordunidif  6382  eliman0  6898  dffv2  6956  elrnrexdm  7061  eldmrexrn  7063  elabrex  7216  elabrexg  7217  elunirn2OLD  7227  f1elima  7238  fliftfun  7287  fliftval  7291  f1oiso2  7327  sorpssuni  7708  sorpssint  7709  onssmin  7768  onminex  7778  fimaproj  8114  frxp3  8130  poseq  8137  tfrlem12  8357  seqomlem2  8419  oawordeulem  8518  oaass  8525  odi  8543  omass  8544  omeulem1  8546  oen0  8550  oelim2  8559  oeeulem  8565  nnawordex  8601  nnaordex2  8603  eldifsucnn  8628  cofon1  8636  cofon2  8637  naddcllem  8640  naddunif  8657  boxcutc  8914  0fi  9013  snfi  9014  snfiOLD  9015  rexdif1en  9122  rexdif1enOLD  9123  findcard  9127  nnfi  9131  pssnn  9132  unfi  9135  onfin  9179  dif1ennnALT  9222  frfi  9232  fisupg  9235  nnsdomg  9246  nnsdomgOLD  9247  pwfir  9266  prfi  9274  fissuni  9308  fipreima  9309  finsschain  9310  indexfi  9311  marypha1lem  9384  eqsup  9407  supmax  9419  fisup2g  9420  fisupcl  9421  supisoex  9426  infmin  9447  fiinfg  9452  fiinf2g  9453  wofib  9498  wemaplem2  9500  card2inf  9508  brwdom2  9526  cnfcom3clem  9658  ssttrcl  9668  ttrcltr  9669  trcl  9681  frmin  9702  r1ordg  9731  r1pwss  9737  tz9.12lem3  9742  tz9.12  9743  r1elwf  9749  tcrank  9837  scottex  9838  scott0  9839  isnumi  9899  onsdom  9949  ondomen  9990  infpwfien  10015  cardaleph  10042  infenaleph  10044  alephfplem4  10060  alephfp2  10062  dfac2b  10084  ackbij1lem18  10189  ackbij1  10190  cflem  10198  cflemOLD  10199  cflecard  10206  cfsuc  10210  cfflb  10212  cofsmo  10222  coftr  10226  fin23lem7  10269  fin23lem11  10270  enfin2i  10274  fin23lem26  10278  isf32lem5  10310  isf34lem4  10330  isfin1-3  10339  fin1a2lem7  10359  axdc3lem4  10406  ttukeylem7  10468  iunfo  10492  ficard  10518  pwcfsdom  10536  fpwwe2lem11  10594  wunex  10692  eltsk2g  10704  grur1  10773  axgroth6  10781  inaprc  10789  nqereu  10882  archnq  10933  genpnmax  10960  ltexpri  10996  prlem936  11000  recexpr  11004  supexpr  11007  negexsr  11055  recexsrlem  11056  recexsr  11060  supsrlem  11064  axrnegex  11115  axrrecex  11116  axpre-sup  11122  1re  11174  dedekind  11337  dedekindle  11338  cnegex  11355  cnegex2  11356  recex  11810  receu  11823  fiminre2  12131  cju  12182  nn2ge  12213  nominpos  12419  zdiv  12604  btwnz  12637  uzwo  12870  ublbneg  12892  lbzbi  12895  zsupss  12896  uzsupss  12899  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem4  12939  rpnnen1lem5  12940  z2ge  13158  qbtwnre  13159  qbtwnxr  13160  xralrple  13165  xrsupsslem  13267  xrinfmsslem  13268  supxrpnf  13278  icc0  13354  uzsup  13825  expnbnd  14197  expmulnbnd  14200  hashkf  14297  hashdom  14344  iswrdi  14482  rtrclreclem1  15023  rtrclreclem2  15025  rtrclreclem3  15026  01sqrex  15215  resqrex  15216  sqrtneg  15233  abs1m  15302  rexanuz  15312  rexuz3  15315  rexuzre  15319  sqreu  15327  o1lo1  15503  climconst  15509  rlimclim1  15511  climshftlem  15540  rlimo1  15583  lo1add  15593  lo1mul  15594  lo1le  15618  isercoll  15634  serf0  15647  zsum  15684  fsum  15686  fsumcvg3  15695  mertenslem1  15850  ntrivcvgn0  15864  ntrivcvgmullem  15867  zprod  15903  fprod  15907  fprodntriv  15908  dvdsval2  16225  dvds0lem  16236  dvds1lem  16237  dvds2lem  16238  odd2np1lem  16310  odd2np1  16311  opeo  16335  omeo  16336  divalglem9  16371  gcdcllem3  16471  lcmcllem  16566  qredeu  16628  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  17504  mreexexlem3d  17607  mreexexlem4d  17608  iscatd  17634  cat1  18059  poslubd  18372  fpwipodrs  18499  ismgmid2  18595  mgmidsssn0  18599  gsumval2a  18612  ismndd  18683  isgrpd2  18888  isgrpd  18890  imasgrp2  18987  mhmmnd  18996  ghmgrp  18998  gaorber  19240  orbsta  19245  cayleyth  19345  pmtrdifel  19410  pmtrdifwrdel  19415  pmtrdifwrdel2  19416  psgnunilem2  19425  psgnunilem3  19426  psgnvalii  19439  pgpfi1  19525  sylow1lem3  19530  sylow1lem5  19532  pgpfi  19535  sylow2alem2  19548  efgredeu  19682  lt6abl  19825  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfaclem1  20013  pgpfaclem3  20015  ablfaclem2  20018  dvdsrmul  20273  dvdsr01  20280  irredrmul  20336  rhmdvdsr  20417  rgspnval  20521  rgspncl  20522  lspf  20880  lspval  20881  lssats2  20906  lspfixed  21038  lspsolvlem  21052  zringlpir  21377  pzriprnglem13  21403  zncyg  21458  cygth  21481  frlmup4  21710  aspval  21782  evlseu  21990  fiinbas  22839  topbas  22859  pptbas  22895  clsval  22924  elcls  22960  neiint  22991  neips  23000  opnneissb  23001  opnssneib  23002  innei  23012  neiptopnei  23019  restbas  23045  neitr  23067  pnfnei  23107  mnfnei  23108  lmconst  23148  iscnp4  23150  cncnpi  23165  cnconst2  23170  cnprest  23176  cnpdis  23180  nrmsep  23244  regsep2  23263  cmpcovf  23278  cmpsub  23287  cmpcld  23289  hauscmplem  23293  conncompid  23318  2ndci  23335  2ndcsb  23336  2ndc1stc  23338  1stcrest  23340  2ndcctbss  23342  2ndcdisj  23343  2ndcomap  23345  2ndcsep  23346  dis2ndc  23347  restlly  23370  islly2  23371  hausllycmp  23381  cldllycmp  23382  lly1stc  23383  dislly  23384  ssref  23399  refref  23400  finlocfin  23407  dissnlocfin  23416  locfindis  23417  llycmpkgen2  23437  cmpkgen  23438  1stckgenlem  23440  elptr  23460  ptbasfi  23468  neitx  23494  ptpjopn  23499  txcnp  23507  ptcnplem  23508  txlly  23523  txnlly  23524  txtube  23527  txcmplem1  23528  tx1stc  23537  txkgen  23539  xkococnlem  23546  txconn  23576  tgqtop  23599  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  reghmph  23680  nrmhmph  23681  fbssfi  23724  opnfbas  23729  isfil2  23743  fsubbas  23754  ssfg  23759  fgss2  23761  fbasrn  23771  filuni  23772  fgtr  23777  ssufl  23805  uffix  23808  elfm2  23835  elfm3  23837  imaelfm  23838  rnelfmlem  23839  rnelfm  23840  fmfnfmlem4  23844  fmfnfm  23845  fmco  23848  ufldom  23849  hausflim  23868  flimcls  23872  hauspwpwf1  23874  flffbas  23882  txflf  23893  fclscf  23912  fclsfnflim  23914  alexsubALTlem4  23937  alexsubALT  23938  tmdgsum2  23983  symgtgp  23993  subgntr  23994  opnsubg  23995  ghmcnp  24002  qustgpopn  24007  tsmsfbas  24015  tsmsxplem1  24040  ustexsym  24103  trust  24117  utoptop  24122  restutop  24125  restutopopn  24126  ustuqtop4  24132  utopsnneiplem  24135  iducn  24170  fmucnd  24179  cfilufg  24180  trcfilu  24181  neipcfilu  24183  imasdsf1olem  24261  blssps  24312  blss  24313  blssexps  24314  blssex  24315  ssblex  24316  blin2  24317  neibl  24389  blcld  24393  metss2  24400  stdbdmopn  24406  met1stc  24409  met2ndci  24410  metrest  24412  prdsxmslem2  24417  metcnp3  24428  metustexhalf  24444  metustfbas  24445  cfilucfil  24447  restmetu  24458  dscopn  24461  ngptgp  24524  nlmvscnlem1  24574  tgioo  24684  tgqioo  24688  xrsmopn  24701  zcld  24702  recld2  24703  zdis  24705  icccmplem1  24711  icccmplem2  24712  xmetdcn2  24726  addcnlem  24753  xrhmeo  24844  cnheibor  24854  cnllycmp  24855  lebnumlem3  24862  lebnum  24863  xlebnum  24864  lebnumii  24865  elpi1i  24946  ipcnlem1  25145  lmnn  25163  iscfil3  25173  cfilres  25196  flimcfil  25214  bcthlem4  25227  bcthlem5  25228  minveclem4c  25325  minveclem2  25326  minveclem3b  25328  minveclem3  25329  minveclem4  25332  minveclem6  25334  ivthlem2  25353  ivth  25355  ivthle  25357  ivthle2  25358  elovolmr  25377  ovolunlem1  25398  ovoliunlem2  25404  ovolicc1  25417  iundisj  25449  iunmbl2  25458  dyadmbllem  25500  volivth  25508  mbflimsup  25567  i1faddlem  25594  i1fmullem  25595  itg2lr  25631  itg2monolem1  25651  limcnlp  25779  ellimc3  25780  limcflf  25782  limciun  25795  rollelem  25893  c1lip1  25902  lhop1lem  25918  ply1divex  26042  ig1peu  26080  elply2  26101  coeeq  26132  plydivlem3  26203  plydivlem4  26204  elqaalem3  26229  qaa  26231  iaa  26233  aareccl  26234  aannenlem2  26237  aalioulem2  26241  aalioulem3  26242  aalioulem5  26244  aalioulem6  26245  aaliou  26246  aaliou2  26248  aaliou3lem8  26253  ulmshftlem  26298  reeff1o  26357  pilem2  26362  pilem3  26363  efif1olem2  26452  efopn  26567  cxpcn3lem  26657  cxpeq  26667  dcubic2  26754  quart  26771  xrlimcnp  26878  ftalem5  26987  ftalem7  26989  sgmnncl  27057  dvdsppwf1o  27096  musum  27101  perfect  27142  dchrptlem1  27175  dchrptlem2  27176  dchrpt  27178  bpos1lem  27193  lgsqrlem4  27260  lgsdchrval  27265  2sqblem  27342  dchrisumlem3  27402  chpdifbndlem2  27465  pntrsumbnd2  27478  pntpbnd1  27497  pntpbnd2  27498  pntpbnd  27499  pntibndlem2  27502  pntibndlem3  27503  pntleme  27519  pntlem3  27520  elno2  27566  sltval2  27568  noreson  27572  sltres  27574  noseponlem  27576  nolesgn2o  27583  nogesgn1o  27585  nodense  27604  nosupfv  27618  nosupres  27619  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  noetalem2  27654  cuteq0  27744  cuteq1  27746  oldlim  27798  cofcutrtime  27835  cofss  27838  coiniss  27839  cutlt  27840  cutmax  27842  cutmin  27843  negsex  27949  negsfo  27959  norecdiv  28093  divs1  28107  precsexlem11  28119  precsex  28120  recsex  28121  elons2d  28160  onscutlt  28165  n0ons  28228  bdayn0sf1o  28259  dfnns2  28261  pw2recs  28323  halfcut  28333  0reno  28348  readdscl  28350  axtgcont  28396  tgcgrxfr  28445  legid  28514  btwnleg  28515  leg0  28519  tghilberti1  28564  tglnpt2  28568  colline  28576  mirreu3  28581  isperp2  28642  colperpex  28660  lnopp2hpgb  28690  hpgerlem  28692  brbtwn  28826  brcgr  28827  brbtwn2  28832  axpasch  28868  axlowdimlem14  28882  axlowdim2  28887  axcontlem2  28892  axcontlem4  28894  axcontlem8  28898  axcontlem10  28900  axcontlem12  28902  fusgrn0degnn0  29427  friendshipgt3  30327  lpni  30409  isgrpoi  30427  vacn  30623  smcnlem  30626  nmosetn0  30694  nmoolb  30700  nmobndi  30704  nmoo0  30720  nmlno0lem  30722  isblo3i  30730  blo3i  30731  blocnilem  30733  ubthlem1  30799  minvecolem2  30804  minvecolem3  30805  minvecolem4c  30808  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  norm1exi  31179  occl  31233  spanval  31262  spancl  31265  shsval2i  31316  ococin  31337  pjoml6i  31518  nmopsetn0  31794  nmfnsetn0  31807  nmoplb  31836  nmfnlb  31853  nmop0  31915  nmfn0  31916  nmlnop0iALT  31924  nmopun  31943  nmcexi  31955  lnconi  31962  lnopcnbd  31965  lnfncnbd  31986  riesz3i  31991  riesz1  31994  cnlnadjlem2  31997  cnlnadjlem8  32003  cnlnadjlem9  32004  adjbd1o  32014  branmfn  32034  opsqrlem1  32069  pjnmopi  32077  strlem1  32179  stri  32186  hstri  32194  cvcon3  32213  cvnbtwn  32215  superpos  32283  shatomici  32287  atcvat4i  32326  mdsymlem2  32333  cdj1i  32362  cdj3i  32370  rexunirn  32421  foresf1o  32433  iundisjf  32518  aciunf1lem  32586  fnpreimac  32595  fgreu  32596  fcnvgreu  32597  xrge0infss  32683  ssnnssfz  32710  iundisjfi  32719  indf1ofs  32789  xreceu  32842  rexdiv  32846  isarchi3  33141  archirngz  33143  archiabllem2a  33148  0nellinds  33341  qtophaus  33826  reff  33829  locfinreflem  33830  cmpcref  33840  dispcmp  33849  tpr2rico  33902  pnfneige0  33941  qqhucn  33982  rrhre  34011  esumcst  34053  esumpcvgval  34068  dmsigagen  34134  rossros  34170  dya2icoseg  34268  dya2iocnrect  34272  dya2iocuni  34274  eulerpartlemgvv  34367  dstfrvunirn  34466  ballotlem4  34490  ballotlemic  34498  ballotlem1c  34499  ballotlemrc  34522  signsw0g  34547  signswmnd  34548  prodfzo03  34594  tgoldbachgt  34654  onvf1odlem4  35093  loop1cycl  35124  umgr2cycllem  35127  umgr2cycl  35128  subfacp1lem3  35169  erdsze2lem2  35191  cnpconn  35217  txpconn  35219  ptpconn  35220  indispconn  35221  connpconn  35222  cvxpconn  35229  cnllysconn  35232  cvmsss2  35261  cvmcov2  35262  cvmopnlem  35265  cvmliftlem14  35284  cvmliftlem15  35285  cvmlift2lem11  35300  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmlift3lem2  35307  cvmlift3lem6  35311  cvmlift3lem9  35314  mthmi  35564  r1peuqusdeg1  35630  br8  35743  br6  35744  br4  35745  dfon2lem9  35779  wzel  35812  wsuclem  35813  wsuclb  35816  imagesset  35941  fvtransport  36020  brcolinear  36047  brsegle  36096  seglerflx  36100  seglemin  36101  btwnsegle  36105  fvray  36129  fvline  36132  hilbert1.1  36142  elhf2  36163  0hf  36165  nn0prpwlem  36310  nn0prpw  36311  fness  36337  fneref  36338  fnessref  36345  refssfne  36346  neibastop2lem  36348  fnemeet1  36354  tailfb  36365  filnetlem4  36369  limsucncmpi  36433  taupilemrplb  37308  relowlssretop  37351  rdgellim  37364  matunitlindflem2  37611  ptrecube  37614  poimirlem4  37618  poimirlem17  37631  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem32  37646  heicant  37649  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  volsupnfl  37659  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem5  37691  unirep  37708  cover2  37709  indexa  37727  frinfm  37729  sdclem1  37737  fdc  37739  incsequz  37742  caushft  37755  istotbnd3  37765  0totbnd  37767  sstotbnd2  37768  sstotbnd  37769  sstotbnd3  37770  isbnd3  37778  ssbnd  37782  equivbnd  37784  prdsbnd  37787  prdstotbnd  37788  cntotbnd  37790  heibor1lem  37803  heiborlem1  37805  heiborlem3  37807  heiborlem6  37810  heiborlem8  37812  bfplem2  37817  rrncmslem  37826  iccbnd  37834  opidonOLD  37846  exidres  37872  isrngod  37892  isgrpda  37949  isdrngo2  37952  igenval  38055  igenidl  38057  prtlem10  38858  lshpnel2N  38978  lsmsat  39001  lssatomic  39004  lcvnbtwn  39018  lfl1  39063  eqlkr  39092  lshpkrlem1  39103  lshpkrex  39111  cvrcon3b  39270  cvrat4  39437  3dim3  39463  ps-2  39472  llni  39502  llnle  39512  lplni  39526  lplnle  39534  lplnexllnN  39558  lvoli  39569  lnatexN  39773  elpaddn0  39794  pclfinN  39894  lhprelat3N  40034  4atexlemex2  40065  4atex  40070  4atex2-0aOLDN  40072  4atex2-0cOLDN  40074  lautcvr  40086  cdleme0ex1N  40217  cdleme50rnlem  40538  cdleme50ex  40553  cdlemg1cex  40582  cdlemkid5  40929  cdlemk  40968  tendoex  40969  cdleml5N  40974  cdlemm10N  41112  dih1dimatlem0  41322  dihjat1lem  41422  dvh3dim2  41442  dvh3dim3N  41443  dochkr1  41472  dochkr1OLDN  41473  lcfrvalsnN  41535  lcfrlem27  41563  lcfrlem37  41573  lcfr  41579  mapd1o  41642  mapdpglem23  41688  hdmap11lem2  41836  primrootsunit1  42085  zdivgd  42325  resubeu  42365  fidomncyc  42523  nacsfix  42700  mzpcompact2lem  42739  eldioph  42746  diophrw  42747  diophin  42760  rexrabdioph  42782  rexzrexnn0  42792  eldioph4b  42799  rencldnfilem  42808  irrapxlem5  42814  irrapxlem6  42815  pell1234qrdich  42849  pell14qrdich  42857  infmrgelbi  42866  pellqrex  42867  pellfundre  42869  pellfundlb  42872  rmxynorm  42907  congrep  42962  acongrep  42969  jm2.27  42997  fnwe2lem2  43040  islssfgi  43061  hbtlem2  43113  hbtlem4  43115  hbtlem5  43117  dgraaub  43137  mpaaeu  43139  aaitgo  43151  unielss  43207  onexgt  43229  onexomgt  43230  onexlimgt  43232  onexoegt  43233  oaordnr  43285  omnord1  43294  oenord1  43305  oaomoencom  43306  oenass  43308  tfsconcatfv2  43329  tfsconcatrn  43331  tfsconcatb0  43333  ofoafo  43345  naddcnffo  43353  oaun3lem1  43363  naddwordnexlem4  43390  sucomisnotcard  43533  clsk1independent  44035  0elaxnul  44973  pwclaxpow  44974  prclaxpr  44975  uniclaxun  44976  omssaxinf2  44978  wfac8prim  44992  restuni3  45112  iinssd  45125  founiiun  45173  wessf1ornlem  45179  founiiun0  45184  unirnmap  45202  dstregt0  45280  uzfissfz  45322  rpgtrecnn  45376  rexabslelem  45414  infrnmptle  45419  infxrunb3rnmpt  45424  infxrpnf  45442  supminfxr  45460  rexanuz2nf  45488  iooiinicc  45540  iooiinioc  45554  uzubioo  45563  climsuse  45606  islptre  45617  limsuppnfdlem  45699  climinf3  45714  limsupmnfuzlem  45724  limsupre3lem  45730  limsupre3uzlem  45733  0cnv  45740  liminfreuzlem  45800  cnrefiisplem  45827  icccncfext  45885  cncficcgt0  45886  dvbdfbdioo  45928  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem9  46007  stoweidlem14  46012  stoweidlem18  46016  stoweidlem21  46019  stoweidlem29  46027  stoweidlem34  46032  stoweidlem35  46033  stoweidlem39  46037  stoweidlem41  46039  stoweidlem45  46043  stoweidlem52  46050  stoweidlem55  46053  stoweidlem57  46055  stoweidlem60  46058  stirlinglem5  46076  stirlinglem13  46084  stirlinglem14  46085  fourierdlem16  46121  fourierdlem20  46125  fourierdlem21  46126  fourierdlem22  46127  fourierdlem25  46130  fourierdlem31  46136  fourierdlem39  46144  fourierdlem41  46146  fourierdlem42  46147  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem77  46181  fourierdlem81  46185  fourierdlem83  46187  fourierdlem103  46207  fourierdlem104  46208  elaa2lem  46231  etransclem47  46279  qndenserrnbl  46293  ioorrnopnlem  46302  ioorrnopnxrlem  46304  intsaluni  46327  salgencntex  46341  subsaliuncllem  46355  sge0resplit  46404  sge0seq  46444  sge0reuz  46445  nnfoctbdjlem  46453  meaiininclem  46484  hoicvrrex  46554  ovnlecvr  46556  ovnlerp  46560  hoidmv1lelem2  46590  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  ovnlecvr2  46608  hoiqssbl  46623  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  iinhoiicclem  46671  smfinflem  46815  smflimsuplem7  46824  sprsymrelfolem2  47494  perfectALTV  47724  9gbo  47775  11gbo  47776  nnsum3primes4  47789  nnsum3primesprm  47791  ssnn0ssfz  48337  lincsumcl  48420  lincscmcl  48421  zlmodzxzldep  48493  ldepsnlinc  48497  line2ylem  48740  line2xlem  48742  sepfsepc  48916  lubsscl  48948  glbsscl  48949  nelsubc3lem  49059  cnelsubclem  49592  aacllem  49790