Theorem rexlimdva 3139

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3137	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ 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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimdvaa  3140  rexlimivv  3180  rexlimdvv  3194  rspceb2dv  3582  ssexnelpss  4070  ralxfrd2  5359  iunopeqop  5477  elsnxp  6257  foco2  7063  elunirn  7207  f1elima  7219  mptcnfimad  7940  releldmdifi  7999  mpoexw  8032  xpord3pred  8104  sexp3  8105  tfrlem9a  8327  seqomlem2  8392  oawordexr  8493  odi  8516  oelimcl  8538  nnawordex  8575  nnaordex  8576  oaabs  8586  oaabs2  8587  omabs  8589  eldifsucnn  8602  coflton  8609  cofon1  8610  cofon2  8611  cofonr  8612  naddunif  8631  ectocld  8731  onfin  9151  dif1ennnALT  9189  isfinite2  9210  isfiniteg  9212  fofinf1o  9244  elfiun  9345  suplub2  9376  supisoex  9390  ordtypelem9  9443  ordtypelem10  9444  brwdom2  9490  brwdom3  9499  ttrcltr  9637  rankr1ai  9722  fodomfi2  9982  infpwfien  9984  dfac12r  10069  ackbij1  10159  cff1  10180  fin23lem21  10261  isf32lem2  10276  fin1a2lem11  10332  fin1a2lem13  10334  ficard  10487  gchina  10622  eltsk2g  10674  tskr1om2  10691  rankcf  10700  inatsk  10701  tskuni  10706  nqereu  10852  ltexnq  10898  1idpr  10952  suplem1pr  10975  supsrlem  11034  axpre-sup  11092  1re  11144  0re  11146  0cnALT  11380  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  suprzcl2  12863  qmulz  12876  elpq  12900  qbtwnre  13126  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  addmodlteq  13881  fsequb  13910  hashdom  14314  ccats1alpha  14555  reuccatpfxs1lem  14681  shftlem  15003  rexuzre  15288  rexico  15289  caubnd  15294  limsupbnd1  15417  limsupbnd2  15418  rlim2lt  15432  rlim3  15433  lo1bdd2  15459  lo1bddrp  15460  o1lo1  15472  climuni  15487  climshftlem  15509  o1co  15521  rlimcn1  15523  climcn1  15527  o1rlimmul  15554  lo1le  15587  rlimno1  15589  isercoll  15603  caurcvg2  15613  serf0  15616  summolem2  15651  zsum  15653  fsum2dlem  15705  geomulcvg  15811  mertenslem2  15820  ntrivcvg  15832  zprod  15872  fprod2dlem  15915  dvds1lem  16206  dvdsexp2im  16266  odd2np1lem  16279  sqoddm1div8z  16293  ltoddhalfle  16300  halfleoddlt  16301  flodddiv4  16354  dvdssqim  16493  dvdsexpim  16494  coprmdvds2  16593  divgcdcoprm0  16604  cncongr1  16606  cncongr2  16607  isprm5  16646  rpexp  16661  pythagtriplem1  16756  iserodd  16775  pc2dvds  16819  difsqpwdvds  16827  oddprmdvds  16843  prmpwdvds  16844  4sqlem11  16895  vdwapun  16914  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  vdwlem10  16930  vdwnnlem1  16935  vdwnnlem3  16937  0ram  16960  ramub1lem2  16967  ramcl  16969  cshwsiun  17039  cshwrepswhash1  17042  firest  17364  imasvscafn  17470  imasmnd2  18711  dfgrp3lem  18980  imasgrp2  18997  issubg4  19087  cycsubm  19143  gaorber  19249  orbsta  19254  pmtr3ncom  19416  psgnran  19456  odmulg  19497  odbezout  19499  gexdvdsi  19524  sylow1lem3  19541  odcau  19545  sylow2alem1  19558  sylow3lem6  19573  lsmelvalm  19592  efgrelexlemb  19691  efgredeu  19693  imasabl  19817  cyggeninv  19824  cygctb  19833  cyggexb  19840  dprdssv  19959  dprddisj2  19982  ablfacrplem  20008  pgpfac1lem2  20018  pgpfac1lem5  20022  ringinvnzdiv  20248  imasring  20278  dvdsrcl2  20314  dvdsrmul1  20317  lss1d  20926  lssats2  20963  lspsn  20965  lmhmima  21011  ring2idlqusb  21277  rngqiprngfulem2  21279  lpiss  21296  dvdsrzring  21428  pzriprnglem5  21452  pzriprnglem8  21455  pzriprnglem10  21457  pzriprnglem11  21458  znunit  21530  znrrg  21532  cygznlem3  21536  frgpcyg  21540  lindfrn  21788  mplcoe5lem  22006  mpfind  22082  gsummoncoe1  22264  mpfpf1  22307  pf1mpf  22308  mat1dimelbas  22427  scmatdmat  22471  scmataddcl  22472  scmatsubcl  22473  scmatmulcl  22474  cpmatacl  22672  chpscmat  22798  tgcl  22925  clsval2  23006  innei  23081  restcld  23128  restcldr  23130  ordtrest2lem  23159  cnprest  23245  lmss  23254  lmcls  23258  lmcnp  23260  isreg2  23333  cmpcovf  23347  cncmp  23348  cmpsub  23356  1stcrest  23409  2ndcrest  23410  1stccnp  23418  restnlly  23438  cldllycmp  23451  locfincmp  23482  txcnpi  23564  pthaus  23594  txtube  23596  txcmplem1  23597  txcmplem2  23598  txlm  23604  xkohaus  23609  xkococnlem  23615  xkococn  23616  kqfvima  23686  kqreglem1  23697  isfild  23814  filuni  23841  isufil2  23864  uffix  23877  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  fmfnfm  23914  fmco  23917  fclsopn  23970  ufilcmp  23988  cnpfcf  23997  alexsublem  24000  alexsubALT  24007  cldsubg  24067  ghmcnp  24071  qustgpopn  24076  tsmsgsum  24095  tsmsres  24100  tsmsxplem1  24109  tsmsxp  24111  isucn2  24234  ucnprima  24237  imasdsf1olem  24329  blssps  24380  blss  24381  blssexps  24382  blssex  24383  mopni3  24450  blcld  24461  metrest  24480  metcnp3  24496  reperflem  24775  icccmplem3  24781  xrge0tsms  24791  mulc1cncf  24866  cncfco  24868  cnheibor  24922  bndth  24925  lebnumlem3  24930  xlebnum  24932  lebnumii  24933  nmhmcn  25088  cfil3i  25237  cmetcaulem  25256  cfilres  25264  bcthlem4  25295  ivthlem2  25421  ivthlem3  25422  ivthicc  25427  cniccbdd  25430  ovolunlem1  25466  ovoliunlem2  25472  ovolshftlem2  25479  ovolicc2  25491  iunmbl2  25526  dyadmax  25567  opnmbllem  25570  subopnmbl  25573  volivth  25576  ismbf3d  25623  mbfimaopn2  25626  mbfaddlem  25629  i1fmullem  25663  mbfi1fseqlem4  25687  bddiblnc  25811  ellimc3  25848  dvlip  25966  dvlip2  25968  c1liplem1  25969  dvgt0lem1  25975  dvivthlem2  25982  dvne0  25984  lhop1lem  25986  lhop2  25988  lhop  25989  tdeglem4  26033  mdegnn0cl  26044  ply1divex  26110  dvdsq1p  26136  ig1peu  26148  elply2  26169  plypf1  26185  plydivex  26273  aalioulem3  26310  aalioulem5  26312  aaliou  26314  ulmshftlem  26366  ulmcau  26372  ulmss  26374  ulmbdd  26375  ulmcn  26376  radcnvlt1  26395  eflogeq  26579  efopn  26635  cxpeq  26735  angpieqvd  26809  xrlimcnp  26946  cxploglim  26956  ftalem2  27052  ftalem7  27057  isppw2  27093  dchrptlem1  27243  dchrptlem3  27245  dchrsum2  27247  lgsdchrval  27333  lgsdchr  27334  gausslemma2dlem1a  27344  lgsquadlem1  27359  2lgsoddprmlem2  27388  dchrisumlem3  27470  dchrisum0fno1  27490  pntlem3  27588  pntleml  27590  ostth3  27617  nosupno  27683  nosupbday  27685  noinfbday  27700  cutsun12  27798  oldssmade  27875  addsproplem2  27978  addsuniflem  28009  addbdaylem  28025  negsid  28049  negsunif  28063  negleft  28066  negright  28067  precsexlem6  28220  precsexlem7  28221  precsexlem11  28225  bdayons  28284  onaddscl  28285  om2noseqlt  28307  noseqrdgfn  28314  n0fincut  28363  bdayn0sf1o  28378  dfnns2  28380  bdaypw2n0bndlem  28471  bdayfinbndlem1  28475  z12negscl  28486  z12zsodd  28490  z12bdaylem  28492  bdayfinlem  28494  recut  28502  elreno2  28503  brcgr  28985  brbtwn2  28990  axbtwnid  29024  axcontlem7  29055  usgrnloopALT  29288  uhgrspansubgrlem  29375  nbuhgr  29428  nbupgr  29429  wwlksnextprop  29997  elwspths2on  30047  elwspths2onw  30048  erclwwlktr  30109  clwwlknscsh  30149  erclwwlkntr  30158  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  3cyclfrgrrn1  30372  frgrregorufr  30412  frgr2wwlk1  30416  ubthlem1  30957  ubthlem3  30959  htthlem  31004  omlsii  31490  spansncol  31655  nmopun  32101  nmcexi  32113  riesz1  32152  elpjrn  32277  cvcon3  32371  chcv1  32442  atcvatlem  32472  chirredi  32481  br8d  32697  xrge0tsmsd  33166  ordtrest2NEWlem  34099  lmxrge0  34129  esumfsup  34247  esumpcvgval  34255  measdivcstALTV  34402  eulerpartlemgh  34555  dstfrvunirn  34652  afsval  34848  onvf1odlem4  35319  erdszelem8  35411  erdszelem11  35414  erdsze2lem2  35417  connpconn  35448  sconnpi1  35452  cvmsss2  35487  cvmfolem  35492  cvmliftmolem2  35495  cvmliftlem15  35511  cvmlift2lem1  35515  cvmlift3lem4  35535  cvmlift3lem5  35536  satfdmlem  35581  fmla1  35600  gonarlem  35607  gonar  35608  goalrlem  35609  goalr  35610  fmla0disjsuc  35611  fmlasucdisj  35612  satffunlem1lem1  35615  satffunlem1lem2  35616  satffunlem2lem1  35617  mrsub0  35729  mrsubcn  35732  msubrn  35742  msubvrs  35773  br8  35969  br6  35970  br4  35971  cgrtriv  36215  btwntriv2  36225  btwncomim  36226  btwnswapid  36230  btwnintr  36232  btwnexch3  36233  btwnouttr2  36235  ifscgr  36257  cgrxfr  36268  btwnxfr  36269  btwnconn3  36316  segcon2  36318  brsegle  36321  seglecgr12im  36323  broutsideof3  36339  linethru  36366  elhf2  36388  opnregcld  36543  cldregopn  36544  neibastop2lem  36573  matunitlindflem1  37864  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem24  37892  poimirlem29  37897  heicant  37903  opnmbllem0  37904  ismblfin  37909  itg2addnclem  37919  itg2addnclem3  37921  itg2gt0cn  37923  ftc1anclem5  37945  ftc2nc  37950  filbcmb  37988  fdc  37993  incsequz  37996  caushft  38009  istotbnd3  38019  equivbnd  38038  cntotbnd  38044  heibor1lem  38057  heibor1  38058  bfplem2  38071  divrngidl  38276  prnc  38315  lshpdisj  39360  cvrcon3b  39650  atnle  39690  hlhgt2  39762  hl0lt1N  39763  hl2at  39778  cvrexchlem  39792  cvratlem  39794  lvolnlelpln  39958  2lplnj  39993  ispsubcl2N  40320  lautcvr  40465  dva1dim  41358  dib1dim  41538  dib1dim2  41541  diclspsn  41567  dih1dimatlem  41702  dihlatat  41710  dihatexv  41711  dihatexv2  41712  lcfrlem9  41923  lcfrlem16  41931  mapdrvallem2  42018  mapd1o  42021  aks6d1c2  42497  elre0re  42621  prjspner1  42981  dffltz  42989  rexlimdv3d  43037  elrfi  43048  isnacs3  43064  eldiophb  43111  eldiophss  43128  diophren  43167  rencldnfilem  43174  pell1234qrdich  43215  pellfundex  43240  lsmfgcl  43428  kercvrlsm  43437  lmhmfgima  43438  lpirlnr  43471  hbtlem2  43478  hbtlem4  43480  hbtlem6  43483  rngunsnply  43523  onexoegt  43598  oaabsb  43648  cantnfresb  43678  omabs2  43686  tfsconcatrev  43702  restuni3  45474  limsupubuz  46068  stoweidlem57  46412  fourierdlem48  46509  fourierdlem49  46510  sge0le  46762  fsetsniunop  47406  cfsetsnfsetfo  47417  fcoresf1  47426  euoreqb  47466  modlt0b  47720  imasetpreimafvbijlemf1  47761  imasetpreimafvbijlemfo  47762  iccpartrn  47787  iccpartiun  47791  iccpartnel  47795  paireqne  47868  reupr  47879  odz2prm2pw  47920  fmtnofac2lem  47925  prmdvdsfmtnof1lem2  47942  2pwp1prm  47946  mod42tp1mod8  47959  lighneallem3  47964  lighneallem4  47967  requad01  47978  requad2  47980  fppr2odd  48088  gbowpos  48116  gbowgt5  48119  gboge9  48121  nnsum4primesodd  48153  nnsum4primesoddALTV  48154  isubgredg  48223  grimcnv  48245  uhgrimedgi  48247  isuspgrim0  48251  isuspgrimlem  48252  gricushgr  48274  clnbgrgrimlem  48290  clnbgrgrim  48291  grimedg  48292  grtrissvtx  48301  stgrusgra  48316  isubgr3stgrlem7  48329  gpgiedgdmellem  48403  gpgusgralem  48413  gpgvtxedg0  48420  gpgvtxedg1  48421  copisnmnd  48526  lidldomn1  48588  affinecomb1  49059  eenglngeehlnmlem2  49095  rrx2vlinest  49098  itsclquadb  49133  aacllem  50157