Theorem rspcev 3613

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2138, ax-11 2155, ax-12 2172. (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 483	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcedv 3606	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥 ∈ 𝐵 𝜑))
5	4	imp 408	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  rspceaimv  3617  rspc2ev  3624  rspc3ev  3628  rspceeqv  3633  reu6i  3724  rspesbca  3875  eliuni  5003  iuneqconst  5008  brralrspcev  5208  wefrc  5670  wereu2  5673  xpdifid  6165  frpomin  6339  onfr  6401  onelssex  6410  ordunidif  6411  eliman0  6929  dffv2  6984  elrnrexdm  7088  eldmrexrn  7090  elabrex  7239  elunirn2OLD  7249  f1elima  7259  fliftfun  7306  fliftval  7310  f1oiso2  7346  sorpssuni  7719  sorpssint  7720  onssmin  7777  onminex  7787  fimaproj  8118  frxp2  8127  frxp3  8134  poseq  8141  tfrlem12  8386  seqomlem2  8448  oawordeulem  8551  oaass  8558  odi  8576  omass  8577  omeulem1  8579  oen0  8583  oelim2  8592  oeeulem  8598  nnawordex  8634  eldifsucnn  8660  cofon1  8668  cofon2  8669  naddcllem  8672  naddunif  8689  boxcutc  8932  snfi  9041  rexdif1en  9155  rexdif1enOLD  9156  findcard  9160  nnfi  9164  pssnn  9165  ssnnfiOLD  9167  unfi  9169  pwfir  9173  onfin  9227  pssnnOLD  9262  dif1ennnALT  9274  frfi  9285  fisupg  9288  nnsdomg  9299  nnsdomgOLD  9300  unfiOLD  9310  fissuni  9354  fipreima  9355  finsschain  9356  indexfi  9357  marypha1lem  9425  eqsup  9448  supmax  9459  fisup2g  9460  fisupcl  9461  supisoex  9466  infmin  9486  fiinfg  9491  fiinf2g  9492  wofib  9537  wemaplem2  9539  card2inf  9547  brwdom2  9565  cnfcom3clem  9697  ssttrcl  9707  ttrcltr  9708  trcl  9720  frmin  9741  r1ordg  9770  r1pwss  9776  tz9.12lem3  9781  tz9.12  9782  r1elwf  9788  tcrank  9876  scottex  9877  scott0  9878  isnumi  9938  onsdom  9988  ondomen  10029  infpwfien  10054  cardaleph  10081  infenaleph  10083  alephfplem4  10099  alephfp2  10101  dfac2b  10122  ackbij1lem18  10229  ackbij1  10230  cflem  10238  cflecard  10245  cfsuc  10249  cfflb  10251  cofsmo  10261  coftr  10265  fin23lem7  10308  fin23lem11  10309  enfin2i  10313  fin23lem26  10317  isf32lem5  10349  isf34lem4  10369  isfin1-3  10378  fin1a2lem7  10398  axdc3lem4  10445  ttukeylem7  10507  iunfo  10531  ficard  10557  pwcfsdom  10575  fpwwe2lem11  10633  wunex  10731  eltsk2g  10743  grur1  10812  axgroth6  10820  inaprc  10828  nqereu  10921  archnq  10972  genpnmax  10999  ltexpri  11035  prlem936  11039  recexpr  11043  supexpr  11046  negexsr  11094  recexsrlem  11095  recexsr  11099  supsrlem  11103  axrnegex  11154  axrrecex  11155  axpre-sup  11161  1re  11211  dedekind  11374  dedekindle  11375  cnegex  11392  cnegex2  11393  recex  11843  receu  11856  fiminre2  12159  cju  12205  nn2ge  12236  nominpos  12446  zdiv  12629  btwnz  12662  uzwo  12892  ublbneg  12914  lbzbi  12917  zsupss  12918  uzsupss  12921  rpnnen1lem1  12959  rpnnen1lem3  12960  rpnnen1lem4  12961  rpnnen1lem5  12962  z2ge  13174  qbtwnre  13175  qbtwnxr  13176  xralrple  13181  xrsupsslem  13283  xrinfmsslem  13284  supxrpnf  13294  icc0  13369  uzsup  13825  expnbnd  14192  expmulnbnd  14195  hashkf  14289  hashdom  14336  iswrdi  14465  rtrclreclem1  15001  rtrclreclem2  15003  rtrclreclem3  15004  01sqrex  15193  resqrex  15194  sqrtneg  15211  abs1m  15279  rexanuz  15289  rexuz3  15292  rexuzre  15296  sqreu  15304  o1lo1  15478  climconst  15484  rlimclim1  15486  climshftlem  15515  rlimo1  15558  lo1add  15568  lo1mul  15569  lo1le  15595  isercoll  15611  serf0  15624  zsum  15661  fsum  15663  fsumcvg3  15672  mertenslem1  15827  ntrivcvgn0  15841  ntrivcvgmullem  15844  zprod  15878  fprod  15882  fprodntriv  15883  dvdsval2  16197  dvds0lem  16207  dvds1lem  16208  dvds2lem  16209  odd2np1lem  16280  odd2np1  16281  opeo  16305  omeo  16306  divalglem9  16341  gcdcllem3  16439  lcmcllem  16530  qredeu  16592  exprmfct  16638  isprm5  16641  odzcllem  16722  reumodprminv  16734  modprm0  16735  nnnn0modprm0  16736  pythagtriplem19  16763  pcprmpw2  16812  pockthi  16837  infpnlem2  16841  vdwlem2  16912  vdwlem10  16920  vdwlem13  16923  ramub1lem1  16956  cshwrepswhash1  17033  imasleval  17484  mreexexlem3d  17587  mreexexlem4d  17588  iscatd  17614  cat1  18044  poslubd  18363  fpwipodrs  18490  ismgmid2  18584  mgmidsssn0  18588  gsumval2a  18601  ismndd  18644  isgrpd2  18839  isgrpd  18841  imasgrp2  18935  mhmmnd  18942  ghmgrp  18944  gaorber  19167  orbsta  19172  cayleyth  19278  pmtrdifel  19343  pmtrdifwrdel  19348  pmtrdifwrdel2  19349  psgnunilem2  19358  psgnunilem3  19359  psgnvalii  19372  pgpfi1  19458  sylow1lem3  19463  sylow1lem5  19465  pgpfi  19468  sylow2alem2  19481  efgredeu  19615  lt6abl  19758  pgpfac1lem3a  19941  pgpfac1lem3  19942  pgpfac1lem5  19944  pgpfaclem1  19946  pgpfaclem3  19948  ablfaclem2  19951  dvdsrmul  20171  dvdsr01  20178  irredrmul  20234  rhmdvdsr  20280  lspf  20578  lspval  20579  lssats2  20604  lspfixed  20734  lspsolvlem  20748  zringlpir  21029  zncyg  21096  cygth  21119  frlmup4  21348  aspval  21419  evlseu  21638  fiinbas  22447  topbas  22467  pptbas  22503  clsval  22533  elcls  22569  neiint  22600  neips  22609  opnneissb  22610  opnssneib  22611  innei  22621  neiptopnei  22628  restbas  22654  neitr  22676  pnfnei  22716  mnfnei  22717  lmconst  22757  iscnp4  22759  cncnpi  22774  cnconst2  22779  cnprest  22785  cnpdis  22789  nrmsep  22853  regsep2  22872  cmpcovf  22887  cmpsub  22896  cmpcld  22898  hauscmplem  22902  conncompid  22927  2ndci  22944  2ndcsb  22945  2ndc1stc  22947  1stcrest  22949  2ndcctbss  22951  2ndcdisj  22952  2ndcomap  22954  2ndcsep  22955  dis2ndc  22956  restlly  22979  islly2  22980  hausllycmp  22990  cldllycmp  22991  lly1stc  22992  dislly  22993  ssref  23008  refref  23009  finlocfin  23016  dissnlocfin  23025  locfindis  23026  llycmpkgen2  23046  cmpkgen  23047  1stckgenlem  23049  elptr  23069  ptbasfi  23077  neitx  23103  ptpjopn  23108  txcnp  23116  ptcnplem  23117  txlly  23132  txnlly  23133  txtube  23136  txcmplem1  23137  tx1stc  23146  txkgen  23148  xkococnlem  23155  txconn  23185  tgqtop  23208  kqreglem1  23237  kqreglem2  23238  kqnrmlem1  23239  kqnrmlem2  23240  reghmph  23289  nrmhmph  23290  fbssfi  23333  opnfbas  23338  isfil2  23352  fsubbas  23363  ssfg  23368  fgss2  23370  fbasrn  23380  filuni  23381  fgtr  23386  ssufl  23414  uffix  23417  elfm2  23444  elfm3  23446  imaelfm  23447  rnelfmlem  23448  rnelfm  23449  fmfnfmlem4  23453  fmfnfm  23454  fmco  23457  ufldom  23458  hausflim  23477  flimcls  23481  hauspwpwf1  23483  flffbas  23491  txflf  23502  fclscf  23521  fclsfnflim  23523  alexsubALTlem4  23546  alexsubALT  23547  tmdgsum2  23592  symgtgp  23602  subgntr  23603  opnsubg  23604  ghmcnp  23611  qustgpopn  23616  tsmsfbas  23624  tsmsxplem1  23649  ustexsym  23712  trust  23726  utoptop  23731  restutop  23734  restutopopn  23735  ustuqtop4  23741  utopsnneiplem  23744  iducn  23780  fmucnd  23789  cfilufg  23790  trcfilu  23791  neipcfilu  23793  imasdsf1olem  23871  blssps  23922  blss  23923  blssexps  23924  blssex  23925  ssblex  23926  blin2  23927  neibl  24002  blcld  24006  metss2  24013  stdbdmopn  24019  met1stc  24022  met2ndci  24023  metrest  24025  prdsxmslem2  24030  metcnp3  24041  metustexhalf  24057  metustfbas  24058  cfilucfil  24060  restmetu  24071  dscopn  24074  ngptgp  24137  nlmvscnlem1  24195  tgioo  24304  tgqioo  24308  xrsmopn  24320  zcld  24321  recld2  24322  zdis  24324  icccmplem1  24330  icccmplem2  24331  xmetdcn2  24345  addcnlem  24372  xrhmeo  24454  cnheibor  24463  cnllycmp  24464  lebnumlem3  24471  lebnum  24472  xlebnum  24473  lebnumii  24474  elpi1i  24554  ipcnlem1  24754  lmnn  24772  iscfil3  24782  cfilres  24805  flimcfil  24823  bcthlem4  24836  bcthlem5  24837  minveclem4c  24934  minveclem2  24935  minveclem3b  24937  minveclem3  24938  minveclem4  24941  minveclem6  24943  ivthlem2  24961  ivth  24963  ivthle  24965  ivthle2  24966  elovolmr  24985  ovolunlem1  25006  ovoliunlem2  25012  ovolicc1  25025  iundisj  25057  iunmbl2  25066  dyadmbllem  25108  volivth  25116  mbflimsup  25175  i1faddlem  25202  i1fmullem  25203  itg2lr  25240  itg2monolem1  25260  limcnlp  25387  ellimc3  25388  limcflf  25390  limciun  25403  rollelem  25498  c1lip1  25506  lhop1lem  25522  ply1divex  25646  ig1peu  25681  elply2  25702  coeeq  25733  plydivlem3  25800  plydivlem4  25801  elqaalem3  25826  qaa  25828  iaa  25830  aareccl  25831  aannenlem2  25834  aalioulem2  25838  aalioulem3  25839  aalioulem5  25841  aalioulem6  25842  aaliou  25843  aaliou2  25845  aaliou3lem8  25850  ulmshftlem  25893  reeff1o  25951  pilem2  25956  pilem3  25957  efif1olem2  26044  efopn  26158  cxpcn3lem  26245  cxpeq  26255  dcubic2  26339  quart  26356  xrlimcnp  26463  ftalem5  26571  ftalem7  26573  sgmnncl  26641  dvdsppwf1o  26680  musum  26685  perfect  26724  dchrptlem1  26757  dchrptlem2  26758  dchrpt  26760  bpos1lem  26775  lgsqrlem4  26842  lgsdchrval  26847  2sqblem  26924  dchrisumlem3  26984  chpdifbndlem2  27047  pntrsumbnd2  27060  pntpbnd1  27079  pntpbnd2  27080  pntpbnd  27081  pntibndlem2  27084  pntibndlem3  27085  pntleme  27101  pntlem3  27102  elno2  27147  sltval2  27149  noreson  27153  sltres  27155  noseponlem  27157  nolesgn2o  27164  nogesgn1o  27166  nodense  27185  nosupfv  27199  nosupres  27200  nosupbnd1lem3  27203  nosupbnd1lem5  27205  nosupbnd2lem1  27208  noinffv  27214  noinfres  27215  noinfbnd1lem3  27218  noinfbnd1lem5  27220  noinfbnd2lem1  27223  noetasuplem4  27229  noetainflem4  27233  noetalem2  27235  cuteq0  27323  cuteq1  27324  oldlim  27371  cofcutrtime  27404  cofss  27407  coiniss  27408  cutlt  27409  negsex  27507  negsfo  27517  norecdiv  27628  divs1  27641  precsexlem11  27653  precsex  27654  recsex  27655  axtgcont  27710  tgcgrxfr  27759  legid  27828  btwnleg  27829  leg0  27833  tghilberti1  27878  tglnpt2  27882  colline  27890  mirreu3  27895  isperp2  27956  colperpex  27974  lnopp2hpgb  28004  hpgerlem  28006  brbtwn  28147  brcgr  28148  brbtwn2  28153  axpasch  28189  axlowdimlem14  28203  axlowdim2  28208  axcontlem2  28213  axcontlem4  28215  axcontlem8  28219  axcontlem10  28221  axcontlem12  28223  fusgrn0degnn0  28746  friendshipgt3  29641  lpni  29721  isgrpoi  29739  vacn  29935  smcnlem  29938  nmosetn0  30006  nmoolb  30012  nmobndi  30016  nmoo0  30032  nmlno0lem  30034  isblo3i  30042  blo3i  30043  blocnilem  30045  ubthlem1  30111  minvecolem2  30116  minvecolem3  30117  minvecolem4c  30120  minvecolem4  30121  minvecolem5  30122  minvecolem6  30123  norm1exi  30491  occl  30545  spanval  30574  spancl  30577  shsval2i  30628  ococin  30649  pjoml6i  30830  nmopsetn0  31106  nmfnsetn0  31119  nmoplb  31148  nmfnlb  31165  nmop0  31227  nmfn0  31228  nmlnop0iALT  31236  nmopun  31255  nmcexi  31267  lnconi  31274  lnopcnbd  31277  lnfncnbd  31298  riesz3i  31303  riesz1  31306  cnlnadjlem2  31309  cnlnadjlem8  31315  cnlnadjlem9  31316  adjbd1o  31326  branmfn  31346  opsqrlem1  31381  pjnmopi  31389  strlem1  31491  stri  31498  hstri  31506  cvcon3  31525  cvnbtwn  31527  superpos  31595  shatomici  31599  atcvat4i  31638  mdsymlem2  31645  cdj1i  31674  cdj3i  31682  rexunirn  31720  foresf1o  31730  iundisjf  31808  aciunf1lem  31875  fnpreimac  31884  fgreu  31885  fcnvgreu  31886  xrge0infss  31961  ssnnssfz  31986  iundisjfi  31995  xreceu  32076  rexdiv  32080  isarchi3  32321  archirngz  32323  archiabllem2a  32328  0nellinds  32472  qtophaus  32805  reff  32808  locfinreflem  32809  cmpcref  32819  dispcmp  32828  tpr2rico  32881  pnfneige0  32920  qqhucn  32961  rrhre  32990  indf1ofs  33013  esumcst  33050  esumpcvgval  33065  dmsigagen  33131  rossros  33167  dya2icoseg  33265  dya2iocnrect  33269  dya2iocuni  33271  eulerpartlemgvv  33364  dstfrvunirn  33462  ballotlem4  33486  ballotlemic  33494  ballotlem1c  33495  ballotlemrc  33518  signsw0g  33556  signswmnd  33557  prodfzo03  33604  tgoldbachgt  33664  loop1cycl  34117  umgr2cycllem  34120  umgr2cycl  34121  subfacp1lem3  34162  erdsze2lem2  34184  cnpconn  34210  txpconn  34212  ptpconn  34213  indispconn  34214  connpconn  34215  cvxpconn  34222  cnllysconn  34225  cvmsss2  34254  cvmcov2  34255  cvmopnlem  34258  cvmliftlem14  34277  cvmliftlem15  34278  cvmlift2lem11  34293  cvmlift2lem12  34294  cvmlift2lem13  34295  cvmlift3lem2  34300  cvmlift3lem6  34304  cvmlift3lem9  34307  mthmi  34557  br8  34715  br6  34716  br4  34717  dfon2lem9  34752  wzel  34785  wsuclem  34786  wsuclb  34789  imagesset  34914  fvtransport  34993  brcolinear  35020  brsegle  35069  seglerflx  35073  seglemin  35074  btwnsegle  35078  fvray  35102  fvline  35105  hilbert1.1  35115  elhf2  35136  0hf  35138  nn0prpwlem  35196  nn0prpw  35197  fness  35223  fneref  35224  fnessref  35231  refssfne  35232  neibastop2lem  35234  fnemeet1  35240  tailfb  35251  filnetlem4  35255  limsucncmpi  35319  taupilemrplb  36190  relowlssretop  36233  rdgellim  36246  matunitlindflem2  36474  ptrecube  36477  poimirlem4  36481  poimirlem17  36494  poimirlem20  36497  poimirlem23  36500  poimirlem24  36501  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  poimirlem32  36509  heicant  36512  mblfinlem1  36514  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  volsupnfl  36522  itg2addnclem  36528  itg2addnclem3  36530  itg2addnc  36531  ftc1anclem5  36554  unirep  36571  cover2  36572  indexa  36590  frinfm  36592  sdclem1  36600  fdc  36602  incsequz  36605  caushft  36618  istotbnd3  36628  0totbnd  36630  sstotbnd2  36631  sstotbnd  36632  sstotbnd3  36633  isbnd3  36641  ssbnd  36645  equivbnd  36647  prdsbnd  36650  prdstotbnd  36651  cntotbnd  36653  heibor1lem  36666  heiborlem1  36668  heiborlem3  36670  heiborlem6  36673  heiborlem8  36675  bfplem2  36680  rrncmslem  36689  iccbnd  36697  opidonOLD  36709  exidres  36735  isrngod  36755  isgrpda  36812  isdrngo2  36815  igenval  36918  igenidl  36920  prtlem10  37724  lshpnel2N  37844  lsmsat  37867  lssatomic  37870  lcvnbtwn  37884  lfl1  37929  eqlkr  37958  lshpkrlem1  37969  lshpkrex  37977  cvrcon3b  38136  cvrat4  38303  3dim3  38329  ps-2  38338  llni  38368  llnle  38378  lplni  38392  lplnle  38400  lplnexllnN  38424  lvoli  38435  lnatexN  38639  elpaddn0  38660  pclfinN  38760  lhprelat3N  38900  4atexlemex2  38931  4atex  38936  4atex2-0aOLDN  38938  4atex2-0cOLDN  38940  lautcvr  38952  cdleme0ex1N  39083  cdleme50rnlem  39404  cdleme50ex  39419  cdlemg1cex  39448  cdlemkid5  39795  cdlemk  39834  tendoex  39835  cdleml5N  39840  cdlemm10N  39978  dih1dimatlem0  40188  dihjat1lem  40288  dvh3dim2  40308  dvh3dim3N  40309  dochkr1  40338  dochkr1OLDN  40339  lcfrvalsnN  40401  lcfrlem27  40429  lcfrlem37  40439  lcfr  40445  mapd1o  40508  mapdpglem23  40554  hdmap11lem2  40702  rspcedvdw  41026  resubeu  41247  nacsfix  41436  mzpcompact2lem  41475  eldioph  41482  diophrw  41483  diophin  41496  rexrabdioph  41518  rexzrexnn0  41528  eldioph4b  41535  rencldnfilem  41544  irrapxlem5  41550  irrapxlem6  41551  pell1234qrdich  41585  pell14qrdich  41593  infmrgelbi  41602  pellqrex  41603  pellfundre  41605  pellfundlb  41608  rmxynorm  41643  congrep  41698  acongrep  41705  jm2.27  41733  fnwe2lem2  41779  islssfgi  41800  hbtlem2  41852  hbtlem4  41854  hbtlem5  41856  dgraaub  41876  mpaaeu  41878  aaitgo  41890  rgspnval  41896  rgspncl  41897  unielss  41953  onexgt  41975  onexomgt  41976  onexlimgt  41978  onexoegt  41979  oaordnr  42032  omnord1  42041  oenord1  42052  oaomoencom  42053  oenass  42055  tfsconcatfv2  42076  tfsconcatrn  42078  tfsconcatb0  42080  ofoafo  42092  naddcnffo  42100  oaun3lem1  42110  naddwordnexlem4  42138  sucomisnotcard  42281  clsk1independent  42783  elabrexg  43714  restuni3  43793  iinssd  43806  founiiun  43861  wessf1ornlem  43868  founiiun0  43874  unirnmap  43893  dstregt0  43978  uzfissfz  44023  rpgtrecnn  44077  rexabslelem  44115  infrnmptle  44120  infxrunb3rnmpt  44125  infxrpnf  44143  supminfxr  44161  rexanuz2nf  44190  iooiinicc  44242  iooiinioc  44256  uzubioo  44267  climsuse  44311  islptre  44322  limsuppnfdlem  44404  climinf3  44419  limsupmnfuzlem  44429  limsupre3lem  44435  limsupre3uzlem  44438  0cnv  44445  liminfreuzlem  44505  cnrefiisplem  44532  icccncfext  44590  cncficcgt0  44591  dvbdfbdioo  44633  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  stoweidlem9  44712  stoweidlem14  44717  stoweidlem18  44721  stoweidlem21  44724  stoweidlem29  44732  stoweidlem34  44737  stoweidlem35  44738  stoweidlem39  44742  stoweidlem41  44744  stoweidlem45  44748  stoweidlem52  44755  stoweidlem55  44758  stoweidlem57  44760  stoweidlem60  44763  stirlinglem5  44781  stirlinglem13  44789  stirlinglem14  44790  fourierdlem16  44826  fourierdlem20  44830  fourierdlem21  44831  fourierdlem22  44832  fourierdlem25  44835  fourierdlem31  44841  fourierdlem39  44849  fourierdlem41  44851  fourierdlem42  44852  fourierdlem47  44856  fourierdlem48  44857  fourierdlem49  44858  fourierdlem51  44860  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem77  44886  fourierdlem81  44890  fourierdlem83  44892  fourierdlem103  44912  fourierdlem104  44913  elaa2lem  44936  etransclem47  44984  qndenserrnbl  44998  ioorrnopnlem  45007  ioorrnopnxrlem  45009  intsaluni  45032  salgencntex  45046  subsaliuncllem  45060  sge0resplit  45109  sge0seq  45149  sge0reuz  45150  nnfoctbdjlem  45158  meaiininclem  45189  hoicvrrex  45259  ovnlecvr  45261  ovnlerp  45265  hoidmv1lelem2  45295  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoilem1  45304  ovnlecvr2  45313  hoiqssbl  45328  ovolval4lem2  45353  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  iinhoiicclem  45376  smfinflem  45520  smflimsuplem7  45529  sprsymrelfolem2  46148  perfectALTV  46378  9gbo  46429  11gbo  46430  nnsum3primes4  46443  nnsum3primesprm  46445  ssnn0ssfz  46979  lincsumcl  47066  lincscmcl  47067  zlmodzxzldep  47139  ldepsnlinc  47143  line2ylem  47391  line2xlem  47393  rspceb2dv  47442  sepfsepc  47514  lubsscl  47547  glbsscl  47548  aacllem  47802