Theorem rspcev 3623

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3139

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144

This theorem is referenced by:  rspceaimv  3628  rspc2ev  3635  rspc3ev  3637  rspceeqv  3638  reu6i  3719  rspesbca  3864  eliuni  4925  iuneqconst  4930  brralrspcev  5126  wefrc  5549  wereu2  5552  xpdifid  6025  onfr  6230  ordunidif  6239  eliman0  6705  dffv2  6756  elrnrexdm  6855  eldmrexrn  6857  elabrex  7002  f1elima  7021  fliftfun  7065  fliftval  7069  f1oiso2  7105  sorpssuni  7458  sorpssint  7459  onssmin  7512  onminex  7522  fimaproj  7829  tfrlem12  8025  seqomlem2  8087  oawordeulem  8180  oaass  8187  odi  8205  omass  8206  omeulem1  8208  oen0  8212  oelim2  8221  oeeulem  8227  nnawordex  8263  boxcutc  8505  snfi  8594  onfin  8709  pssnn  8736  ssnnfi  8737  dif1en  8751  findcard  8757  frfi  8763  fisupg  8766  nnsdomg  8777  unfi  8785  fissuni  8829  fipreima  8830  finsschain  8831  indexfi  8832  marypha1lem  8897  eqsup  8920  supmax  8931  fisup2g  8932  fisupcl  8933  supisoex  8938  infmin  8958  fiinfg  8963  fiinf2g  8964  wofib  9009  wemaplem2  9011  card2inf  9019  brwdom2  9037  cnfcom3clem  9168  trcl  9170  r1ordg  9207  r1pwss  9213  tz9.12lem3  9218  tz9.12  9219  r1elwf  9225  tcrank  9313  scottex  9314  scott0  9315  isnumi  9375  onsdom  9425  ondomen  9463  infpwfien  9488  cardaleph  9515  infenaleph  9517  alephfplem4  9533  alephfp2  9535  dfac2b  9556  ackbij1lem18  9659  ackbij1  9660  cflem  9668  cflecard  9675  cfsuc  9679  cfflb  9681  cofsmo  9691  coftr  9695  fin23lem7  9738  fin23lem11  9739  enfin2i  9743  fin23lem26  9747  isf32lem5  9779  isf34lem4  9799  isfin1-3  9808  fin1a2lem7  9828  axdc3lem4  9875  ttukeylem7  9937  iunfo  9961  ficard  9987  pwcfsdom  10005  fpwwe2lem12  10063  wunex  10161  eltsk2g  10173  grur1  10242  axgroth6  10250  inaprc  10258  nqereu  10351  archnq  10402  genpnmax  10429  ltexpri  10465  prlem936  10469  recexpr  10473  supexpr  10476  negexsr  10524  recexsrlem  10525  recexsr  10529  supsrlem  10533  axrnegex  10584  axrrecex  10585  axpre-sup  10591  1re  10641  dedekind  10803  dedekindle  10804  cnegex  10821  cnegex2  10822  recex  11272  receu  11285  cju  11634  nn2ge  11665  nominpos  11875  zdiv  12053  btwnz  12085  uzwo  12312  ublbneg  12334  lbzbi  12337  zsupss  12338  uzsupss  12341  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem4  12380  rpnnen1lem5  12381  z2ge  12592  qbtwnre  12593  qbtwnxr  12594  xralrple  12599  xrsupsslem  12701  xrinfmsslem  12702  supxrpnf  12712  icc0  12787  uzsup  13232  expnbnd  13594  expmulnbnd  13597  hashkf  13693  hashdom  13741  iswrdi  13866  rtrclreclem1  14417  rtrclreclem2  14418  rtrclreclem3  14419  01sqrex  14609  resqrex  14610  sqrtneg  14627  abs1m  14695  rexanuz  14705  rexuz3  14708  rexuzre  14712  sqreu  14720  o1lo1  14894  climconst  14900  rlimclim1  14902  climshftlem  14931  rlimo1  14973  lo1add  14983  lo1mul  14984  lo1le  15008  isercoll  15024  serf0  15037  zsum  15075  fsum  15077  fsumcvg3  15086  mertenslem1  15240  ntrivcvgn0  15254  ntrivcvgmullem  15257  zprod  15291  fprod  15295  fprodntriv  15296  dvdsval2  15610  dvds0lem  15620  dvds1lem  15621  dvds2lem  15622  odd2np1lem  15689  odd2np1  15690  opeo  15714  omeo  15715  divalglem9  15752  gcdcllem3  15850  lcmcllem  15940  qredeu  16002  exprmfct  16048  isprm5  16051  odzcllem  16129  reumodprminv  16141  modprm0  16142  nnnn0modprm0  16143  pythagtriplem19  16170  pcprmpw2  16218  pockthi  16243  infpnlem2  16247  vdwlem2  16318  vdwlem10  16326  vdwlem13  16329  ramub1lem1  16362  cshwrepswhash1  16436  imasleval  16814  mreexexlem3d  16917  mreexexlem4d  16918  iscatd  16944  poslubd  17758  fpwipodrs  17774  ismgmid2  17878  mgmidsssn0  17882  gsumval2a  17895  ismndd  17933  isgrpd2  18123  isgrpd  18125  imasgrp2  18214  mhmmnd  18221  ghmgrp  18223  gaorber  18438  orbsta  18443  cayleyth  18543  pmtrdifel  18608  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem2  18623  psgnunilem3  18624  psgnvalii  18637  pgpfi1  18720  sylow1lem3  18725  sylow1lem5  18727  pgpfi  18730  sylow2alem2  18743  efgredeu  18878  lt6abl  19015  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfac1lem5  19201  pgpfaclem1  19203  pgpfaclem3  19205  ablfaclem2  19208  dvdsrmul  19398  dvdsr01  19405  irredrmul  19457  lspf  19746  lspval  19747  lssats2  19772  lspfixed  19900  lspsolvlem  19914  aspval  20102  evlseu  20296  zringlpir  20636  zncyg  20695  cygth  20718  frlmup4  20945  fiinbas  21560  topbas  21580  pptbas  21616  clsval  21645  elcls  21681  neiint  21712  neips  21721  opnneissb  21722  opnssneib  21723  innei  21733  neiptopnei  21740  restbas  21766  neitr  21788  pnfnei  21828  mnfnei  21829  lmconst  21869  iscnp4  21871  cncnpi  21886  cnconst2  21891  cnprest  21897  cnpdis  21901  nrmsep  21965  regsep2  21984  cmpcovf  21999  cmpsub  22008  cmpcld  22010  hauscmplem  22014  conncompid  22039  2ndci  22056  2ndcsb  22057  2ndc1stc  22059  1stcrest  22061  2ndcctbss  22063  2ndcdisj  22064  2ndcomap  22066  2ndcsep  22067  dis2ndc  22068  restlly  22091  islly2  22092  hausllycmp  22102  cldllycmp  22103  lly1stc  22104  dislly  22105  ssref  22120  refref  22121  finlocfin  22128  dissnlocfin  22137  locfindis  22138  llycmpkgen2  22158  cmpkgen  22159  1stckgenlem  22161  elptr  22181  ptbasfi  22189  neitx  22215  ptpjopn  22220  txcnp  22228  ptcnplem  22229  txlly  22244  txnlly  22245  txtube  22248  txcmplem1  22249  tx1stc  22258  txkgen  22260  xkococnlem  22267  txconn  22297  tgqtop  22320  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  reghmph  22401  nrmhmph  22402  fbssfi  22445  opnfbas  22450  isfil2  22464  fsubbas  22475  ssfg  22480  fgss2  22482  fbasrn  22492  filuni  22493  fgtr  22498  ssufl  22526  uffix  22529  elfm2  22556  elfm3  22558  imaelfm  22559  rnelfmlem  22560  rnelfm  22561  fmfnfmlem4  22565  fmfnfm  22566  fmco  22569  ufldom  22570  hausflim  22589  flimcls  22593  hauspwpwf1  22595  flffbas  22603  txflf  22614  fclscf  22633  fclsfnflim  22635  alexsubALTlem4  22658  alexsubALT  22659  tmdgsum2  22704  symgtgp  22714  subgntr  22715  opnsubg  22716  ghmcnp  22723  qustgpopn  22728  tsmsfbas  22736  tsmsxplem1  22761  ustexsym  22824  elrnust  22833  trust  22838  utoptop  22843  restutop  22846  restutopopn  22847  ustuqtop4  22853  utopsnneiplem  22856  iducn  22892  fmucnd  22901  cfilufg  22902  trcfilu  22903  neipcfilu  22905  imasdsf1olem  22983  blssps  23034  blss  23035  blssexps  23036  blssex  23037  ssblex  23038  blin2  23039  neibl  23111  blcld  23115  metss2  23122  stdbdmopn  23128  met1stc  23131  met2ndci  23132  metrest  23134  prdsxmslem2  23139  metcnp3  23150  metuval  23159  metustexhalf  23166  metustfbas  23167  cfilucfil  23169  restmetu  23180  dscopn  23183  ngptgp  23245  nlmvscnlem1  23295  tgioo  23404  tgqioo  23408  xrsmopn  23420  zcld  23421  recld2  23422  zdis  23424  icccmplem1  23430  icccmplem2  23431  xmetdcn2  23445  addcnlem  23472  xrhmeo  23550  cnheibor  23559  cnllycmp  23560  lebnumlem3  23567  lebnum  23568  xlebnum  23569  lebnumii  23570  elpi1i  23650  ipcnlem1  23848  lmnn  23866  iscfil3  23876  cfilres  23899  flimcfil  23917  bcthlem4  23930  bcthlem5  23931  minveclem4c  24028  minveclem2  24029  minveclem3b  24031  minveclem3  24032  minveclem4  24035  minveclem6  24037  ivthlem2  24053  ivth  24055  ivthle  24057  ivthle2  24058  elovolmr  24077  ovolunlem1  24098  ovoliunlem2  24104  ovolicc1  24117  iundisj  24149  iunmbl2  24158  dyadmbllem  24200  volivth  24208  mbflimsup  24267  i1faddlem  24294  i1fmullem  24295  itg2lr  24331  itg2monolem1  24351  limcnlp  24476  ellimc3  24477  limcflf  24479  limciun  24492  rollelem  24586  c1lip1  24594  lhop1lem  24610  ply1divex  24730  ig1peu  24765  elply2  24786  coeeq  24817  plydivlem3  24884  plydivlem4  24885  elqaalem3  24910  qaa  24912  iaa  24914  aareccl  24915  aannenlem2  24918  aalioulem2  24922  aalioulem3  24923  aalioulem5  24925  aalioulem6  24926  aaliou  24927  aaliou2  24929  aaliou3lem8  24934  ulmshftlem  24977  reeff1o  25035  pilem2  25040  pilem3  25041  efif1olem2  25127  efopn  25241  cxpcn3lem  25328  cxpeq  25338  dcubic2  25422  quart  25439  xrlimcnp  25546  ftalem5  25654  ftalem7  25656  sgmnncl  25724  dvdsppwf1o  25763  musum  25768  perfect  25807  dchrptlem1  25840  dchrptlem2  25841  dchrpt  25843  bpos1lem  25858  lgsqrlem4  25925  lgsdchrval  25930  2sqblem  26007  dchrisumlem3  26067  chpdifbndlem2  26130  pntrsumbnd2  26143  pntpbnd1  26162  pntpbnd2  26163  pntpbnd  26164  pntibndlem2  26167  pntibndlem3  26168  pntleme  26184  pntlem3  26185  axtgcont  26255  tgcgrxfr  26304  legid  26373  btwnleg  26374  leg0  26378  tghilberti1  26423  tglnpt2  26427  colline  26435  mirreu3  26440  isperp2  26501  colperpex  26519  lnopp2hpgb  26549  hpgerlem  26551  brbtwn  26685  brcgr  26686  brbtwn2  26691  axpasch  26727  axlowdimlem14  26741  axlowdim2  26746  axcontlem2  26751  axcontlem4  26753  axcontlem8  26757  axcontlem10  26759  axcontlem12  26761  fusgrn0degnn0  27281  friendshipgt3  28177  lpni  28257  isgrpoi  28275  vacn  28471  smcnlem  28474  nmosetn0  28542  nmoolb  28548  nmobndi  28552  nmoo0  28568  nmlno0lem  28570  isblo3i  28578  blo3i  28579  blocnilem  28581  ubthlem1  28647  minvecolem2  28652  minvecolem3  28653  minvecolem4c  28656  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  norm1exi  29027  occl  29081  spanval  29110  spancl  29113  shsval2i  29164  ococin  29185  pjoml6i  29366  nmopsetn0  29642  nmfnsetn0  29655  nmoplb  29684  nmfnlb  29701  nmop0  29763  nmfn0  29764  nmlnop0iALT  29772  nmopun  29791  nmcexi  29803  lnconi  29810  lnopcnbd  29813  lnfncnbd  29834  riesz3i  29839  riesz1  29842  cnlnadjlem2  29845  cnlnadjlem8  29851  cnlnadjlem9  29852  adjbd1o  29862  branmfn  29882  opsqrlem1  29917  pjnmopi  29925  strlem1  30027  stri  30034  hstri  30042  cvcon3  30061  cvnbtwn  30063  superpos  30131  shatomici  30135  atcvat4i  30174  mdsymlem2  30181  cdj1i  30210  cdj3i  30218  rexunirn  30256  foresf1o  30265  iundisjf  30339  elunirn2  30396  aciunf1lem  30407  fnpreimac  30416  fgreu  30417  fcnvgreu  30418  xrge0infss  30484  ssnnssfz  30510  iundisjfi  30519  xreceu  30598  rexdiv  30602  isarchi3  30816  archirngz  30818  archiabllem2a  30823  rhmdvdsr  30891  0nellinds  30935  qtophaus  31100  reff  31103  locfinreflem  31104  cmpcref  31114  dispcmp  31123  metidval  31130  pstmval  31135  tpr2rico  31155  pnfneige0  31194  qqhucn  31233  rrhre  31262  indf1ofs  31285  esumcst  31322  esumpcvgval  31337  dmsigagen  31403  rossros  31439  dya2icoseg  31535  dya2iocnrect  31539  dya2iocuni  31541  eulerpartlemgvv  31634  dstfrvunirn  31732  ballotlem4  31756  ballotlemic  31764  ballotlem1c  31765  ballotlemrc  31788  signsw0g  31826  signswmnd  31827  prodfzo03  31874  tgoldbachgt  31934  loop1cycl  32384  umgr2cycllem  32387  umgr2cycl  32388  subfacp1lem3  32429  erdsze2lem2  32451  cnpconn  32477  txpconn  32479  ptpconn  32480  indispconn  32481  connpconn  32482  cvxpconn  32489  cnllysconn  32492  cvmsss2  32521  cvmcov2  32522  cvmopnlem  32525  cvmliftlem14  32544  cvmliftlem15  32545  cvmlift2lem11  32560  cvmlift2lem12  32561  cvmlift2lem13  32562  cvmlift3lem2  32567  cvmlift3lem6  32571  cvmlift3lem9  32574  mthmi  32824  br8  32992  br6  32993  br4  32994  dfon2lem9  33036  trpredtr  33069  dftrpred3g  33072  frpomin  33078  frmin  33084  poseq  33095  wzel  33111  wsuclem  33112  wsuclb  33115  elno2  33161  sltval2  33163  noreson  33167  sltres  33169  noseponlem  33171  nolesgn2o  33178  nodense  33196  nosupfv  33206  nosupres  33207  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2lem1  33215  noetalem3  33219  noetalem5  33221  imagesset  33414  fvtransport  33493  brcolinear  33520  brsegle  33569  seglerflx  33573  seglemin  33574  btwnsegle  33578  fvray  33602  fvline  33605  hilbert1.1  33615  elhf2  33636  0hf  33638  nn0prpwlem  33670  nn0prpw  33671  fness  33697  fneref  33698  fnessref  33705  refssfne  33706  neibastop2lem  33708  fnemeet1  33714  tailfb  33725  filnetlem4  33729  limsucncmpi  33793  taupilemrplb  34604  relowlssretop  34647  rdgellim  34660  matunitlindflem2  34904  ptrecube  34907  poimirlem4  34911  poimirlem17  34924  poimirlem20  34927  poimirlem23  34930  poimirlem24  34931  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  poimirlem32  34939  heicant  34942  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  volsupnfl  34952  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  ftc1anclem5  34986  unirep  35003  cover2  35004  indexa  35023  frinfm  35025  sdclem1  35033  fdc  35035  incsequz  35038  caushft  35051  istotbnd3  35064  0totbnd  35066  sstotbnd2  35067  sstotbnd  35068  sstotbnd3  35069  isbnd3  35077  ssbnd  35081  equivbnd  35083  prdsbnd  35086  prdstotbnd  35087  cntotbnd  35089  heibor1lem  35102  heiborlem1  35104  heiborlem3  35106  heiborlem6  35109  heiborlem8  35111  bfplem2  35116  rrncmslem  35125  iccbnd  35133  opidonOLD  35145  exidres  35171  isrngod  35191  isgrpda  35248  isdrngo2  35251  igenval  35354  igenidl  35356  prtlem10  36016  lshpnel2N  36136  lsmsat  36159  lssatomic  36162  lcvnbtwn  36176  lfl1  36221  eqlkr  36250  lshpkrlem1  36261  lshpkrex  36269  cvrcon3b  36428  cvrat4  36594  3dim3  36620  ps-2  36629  llni  36659  llnle  36669  lplni  36683  lplnle  36691  lplnexllnN  36715  lvoli  36726  lnatexN  36930  elpaddn0  36951  pclfinN  37051  lhprelat3N  37191  4atexlemex2  37222  4atex  37227  4atex2-0aOLDN  37229  4atex2-0cOLDN  37231  lautcvr  37243  cdleme0ex1N  37374  cdleme50rnlem  37695  cdleme50ex  37710  cdlemg1cex  37739  cdlemkid5  38086  cdlemk  38125  tendoex  38126  cdleml5N  38131  cdlemm10N  38269  dih1dimatlem0  38479  dihjat1lem  38579  dvh3dim2  38599  dvh3dim3N  38600  dochkr1  38629  dochkr1OLDN  38630  lcfrvalsnN  38692  lcfrlem27  38720  lcfrlem37  38730  lcfr  38736  mapd1o  38799  mapdpglem23  38845  hdmap11lem2  38993  resubeu  39256  nacsfix  39358  mzpcompact2lem  39397  eldioph  39404  diophrw  39405  diophin  39418  rexrabdioph  39440  rexzrexnn0  39450  eldioph4b  39457  rencldnfilem  39466  irrapxlem5  39472  irrapxlem6  39473  pell1234qrdich  39507  pell14qrdich  39515  infmrgelbi  39524  pellqrex  39525  pellfundre  39527  pellfundlb  39530  rmxynorm  39564  congrep  39619  acongrep  39626  jm2.27  39654  fnwe2lem2  39700  islssfgi  39721  hbtlem2  39773  hbtlem4  39775  hbtlem5  39777  dgraaub  39797  mpaaeu  39799  aaitgo  39811  rgspnval  39817  rgspncl  39818  clsk1independent  40445  elabrexg  41352  restuni3  41433  iinssd  41446  founiiun  41484  wessf1ornlem  41494  founiiun0  41500  unirnmap  41520  dstregt0  41596  uzfissfz  41643  fiminre2  41695  rpgtrecnn  41698  rexabslelem  41741  infrnmptle  41746  infxrunb3rnmpt  41751  infxrpnf  41770  supminfxr  41789  iooiinicc  41867  iooiinioc  41881  uzubioo  41892  climsuse  41938  islptre  41949  limsuppnfdlem  42031  climinf3  42046  limsupmnfuzlem  42056  limsupre3lem  42062  limsupre3uzlem  42065  0cnv  42072  liminfreuzlem  42132  cnrefiisplem  42159  icccncfext  42219  cncficcgt0  42220  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweidlem9  42343  stoweidlem14  42348  stoweidlem18  42352  stoweidlem21  42355  stoweidlem29  42363  stoweidlem34  42368  stoweidlem35  42369  stoweidlem39  42373  stoweidlem41  42375  stoweidlem45  42379  stoweidlem52  42386  stoweidlem55  42389  stoweidlem57  42391  stoweidlem60  42394  stirlinglem5  42412  stirlinglem13  42420  stirlinglem14  42421  fourierdlem16  42457  fourierdlem20  42461  fourierdlem21  42462  fourierdlem22  42463  fourierdlem25  42466  fourierdlem31  42472  fourierdlem39  42480  fourierdlem41  42482  fourierdlem42  42483  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem51  42491  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem77  42517  fourierdlem81  42521  fourierdlem83  42523  fourierdlem103  42543  fourierdlem104  42544  elaa2lem  42567  etransclem47  42615  qndenserrnbl  42629  ioorrnopnlem  42638  ioorrnopnxrlem  42640  intsaluni  42661  salgencntex  42675  subsaliuncllem  42689  sge0resplit  42737  sge0seq  42777  sge0reuz  42778  nnfoctbdjlem  42786  meaiininclem  42817  hoicvrrex  42887  ovnlecvr  42889  ovnlerp  42893  hoidmv1lelem2  42923  hoidmvlelem2  42927  hoidmvlelem3  42928  ovnhoilem1  42932  ovnlecvr2  42941  hoiqssbl  42956  ovolval4lem2  42981  ovolval5lem2  42984  ovnovollem1  42987  ovnovollem2  42988  iinhoiicclem  43004  smfinflem  43140  smflimsuplem7  43149  sprsymrelfolem2  43704  perfectALTV  43937  9gbo  43988  11gbo  43989  nnsum3primes4  44002  nnsum3primesprm  44004  ssnn0ssfz  44446  lincsumcl  44535  lincscmcl  44536  zlmodzxzldep  44608  ldepsnlinc  44612  line2ylem  44787  line2xlem  44789  aacllem  44951