Theorem rexlimdva 3162

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 416	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3160	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexlimdvaa  3163  rexlimivv  3203  rexlimdvv  3217  rspceb2dv  3585  ssexnelpss  4070  ralxfrd2  5368  iunopeqop  5489  iunopeqopOLD  5490  elsnxp  6274  foco2  7086  elunirn  7231  f1elima  7243  mptcnfimad  7963  releldmdifi  8022  mpoexw  8055  xpord3pred  8127  sexp3  8128  tfrlem9a  8352  seqomlem2  8417  oawordexr  8520  odi  8543  oelimcl  8565  nnawordex  8602  nnaordex  8603  oaabs  8613  oaabs2  8614  omabs  8616  eldifsucnn  8629  coflton  8636  cofon1  8637  cofon2  8638  cofonr  8639  naddunif  8659  ectocld  8759  onfin  9179  dif1ennnALT  9217  isfinite2  9238  isfiniteg  9240  fofinf1o  9272  elfiun  9373  suplub2  9404  supisoex  9418  ordtypelem9  9471  ordtypelem10  9472  brwdom2  9518  brwdom3  9527  ttrcltr  9668  rankr1ai  9753  fodomfi2  10013  infpwfien  10015  dfac12r  10100  ackbij1  10190  cff1  10212  fin23lem21  10293  isf32lem2  10308  fin1a2lem11  10364  fin1a2lem13  10366  ficard  10519  gchina  10654  eltsk2g  10706  tskr1om2  10723  rankcf  10732  inatsk  10733  tskuni  10738  nqereu  10884  ltexnq  10930  1idpr  10984  suplem1pr  11007  supsrlem  11066  axpre-sup  11124  1re  11178  0re  11180  0cnALT  11415  supaddc  12156  supadd  12157  supmul1  12158  supmul  12161  suprzcl2  12936  qmulz  12949  elpq  12973  qbtwnre  13199  ioo0  13371  ico0  13392  ioc0  13393  icc0  13394  addmodlteq  13956  fsequb  13985  hashdom  14389  ccats1alpha  14630  reuccatpfxs1lem  14756  shftlem  15078  rexuzre  15363  rexico  15364  caubnd  15369  limsupbnd1  15492  limsupbnd2  15493  rlim2lt  15507  rlim3  15508  lo1bdd2  15534  lo1bddrp  15535  o1lo1  15547  climuni  15562  climshftlem  15584  o1co  15596  rlimcn1  15598  climcn1  15602  o1rlimmul  15629  lo1le  15662  rlimno1  15664  isercoll  15678  caurcvg2  15688  serf0  15691  summolem2  15726  zsum  15728  fsum2dlem  15780  geomulcvg  15889  mertenslem2  15898  ntrivcvg  15910  zprod  15950  fprod2dlem  15993  dvds1lem  16284  dvdsexp2im  16344  odd2np1lem  16357  sqoddm1div8z  16371  ltoddhalfle  16378  halfleoddlt  16379  flodddiv4  16432  dvdssqim  16571  dvdsexpim  16572  coprmdvds2  16671  divgcdcoprm0  16682  cncongr1  16684  cncongr2  16685  isprm5  16725  rpexp  16740  pythagtriplem1  16835  iserodd  16854  pc2dvds  16898  difsqpwdvds  16906  oddprmdvds  16922  prmpwdvds  16923  4sqlem11  16974  vdwapun  16993  vdwlem2  17001  vdwlem6  17005  vdwlem8  17007  vdwlem10  17009  vdwnnlem1  17014  vdwnnlem3  17016  0ram  17039  ramub1lem2  17046  ramcl  17048  cshwsiun  17118  cshwrepswhash1  17121  firest  17444  imasvscafn  17550  imasmnd2  18791  dfgrp3lem  19063  imasgrp2  19080  issubg4  19170  cycsubm  19226  gaorber  19331  orbsta  19336  pmtr3ncom  19498  psgnran  19538  odmulg  19579  odbezout  19581  gexdvdsi  19606  sylow1lem3  19623  odcau  19627  sylow2alem1  19640  sylow3lem6  19655  lsmelvalm  19674  efgrelexlemb  19773  efgredeu  19775  imasabl  19899  cyggeninv  19906  cygctb  19915  cyggexb  19922  dprdssv  20041  dprddisj2  20064  ablfacrplem  20090  pgpfac1lem2  20100  pgpfac1lem5  20104  ringinvnzdiv  20330  imasring  20358  dvdsrcl2  20394  dvdsrmul1  20397  lss1d  21010  lssats2  21047  lspsn  21049  lmhmima  21094  ring2idlqusb  21360  rngqiprngfulem2  21362  lpiss  21379  dvdsrzring  21493  pzriprnglem5  21517  pzriprnglem8  21520  pzriprnglem10  21522  pzriprnglem11  21523  znunit  21595  znrrg  21597  cygznlem3  21601  frgpcyg  21605  lindfrn  21853  mplcoe5lem  22072  mpfind  22148  gsummoncoe1  22351  mpfpf1  22394  pf1mpf  22395  mat1dimelbas  22511  scmatdmat  22555  scmataddcl  22556  scmatsubcl  22557  scmatmulcl  22558  cpmatacl  22756  chpscmat  22882  tgcl  23009  clsval2  23090  innei  23165  restcld  23212  restcldr  23214  ordtrest2lem  23243  cnprest  23329  lmss  23338  lmcls  23342  lmcnp  23344  isreg2  23417  cmpcovf  23431  cncmp  23432  cmpsub  23440  1stcrest  23493  2ndcrest  23494  1stccnp  23502  restnlly  23522  cldllycmp  23535  locfincmp  23566  txcnpi  23648  pthaus  23678  txtube  23680  txcmplem1  23681  txcmplem2  23682  txlm  23688  xkohaus  23693  xkococnlem  23699  xkococn  23700  kqfvima  23770  kqreglem1  23781  isfild  23898  filuni  23925  isufil2  23948  uffix  23961  rnelfm  23993  fmfnfmlem2  23995  fmfnfmlem4  23997  fmfnfm  23998  fmco  24001  fclsopn  24054  ufilcmp  24072  cnpfcf  24081  alexsublem  24084  alexsubALT  24091  cldsubg  24151  ghmcnp  24155  qustgpopn  24160  tsmsgsum  24179  tsmsres  24184  tsmsxplem1  24193  tsmsxp  24195  isucn2  24318  ucnprima  24321  imasdsf1olem  24413  blssps  24464  blss  24465  blssexps  24466  blssex  24467  mopni3  24534  blcld  24545  metrest  24564  metcnp3  24580  reperflem  24859  icccmplem3  24865  xrge0tsms  24875  mulc1cncf  24947  cncfco  24949  cnheibor  24997  bndth  25000  lebnumlem3  25005  xlebnum  25007  lebnumii  25008  nmhmcn  25162  cfil3i  25311  cmetcaulem  25330  cfilres  25338  bcthlem4  25369  ivthlem2  25494  ivthlem3  25495  ivthicc  25500  cniccbdd  25503  ovolunlem1  25539  ovoliunlem2  25545  ovolshftlem2  25552  ovolicc2  25564  iunmbl2  25599  dyadmax  25640  opnmbllem  25643  subopnmbl  25646  volivth  25649  ismbf3d  25696  mbfimaopn2  25699  mbfaddlem  25702  i1fmullem  25736  mbfi1fseqlem4  25760  bddiblnc  25884  ellimc3  25921  dvlip  26035  dvlip2  26037  c1liplem1  26038  dvgt0lem1  26044  dvivthlem2  26051  dvne0  26053  lhop1lem  26055  lhop2  26057  lhop  26058  tdeglem4  26100  mdegnn0cl  26111  ply1divex  26177  dvdsq1p  26203  ig1peu  26215  elply2  26236  plypf1  26252  plydivex  26338  aalioulem3  26375  aalioulem5  26377  aaliou  26379  ulmshftlem  26429  ulmcau  26435  ulmss  26437  ulmbdd  26438  ulmcn  26439  radcnvlt1  26458  eflogeq  26644  efopn  26700  cxpeq  26799  angpieqvd  26873  xrlimcnp  27010  cxploglim  27019  ftalem2  27115  ftalem7  27120  isppw2  27156  dchrptlem1  27305  dchrptlem3  27307  dchrsum2  27309  lgsdchrval  27395  lgsdchr  27396  gausslemma2dlem1a  27406  lgsquadlem1  27421  2lgsoddprmlem2  27450  dchrisumlem3  27532  dchrisum0fno1  27552  pntlem3  27650  pntleml  27652  ostth3  27679  nosupno  27744  nosupbday  27746  noinfbday  27761  cutsun12  27860  oldssmade  27937  addsproplem2  28040  addsuniflem  28071  addbdaylem  28087  negsid  28111  negsunif  28125  negleft  28128  negright  28129  precsexlem6  28282  precsexlem7  28283  precsexlem11  28287  bdayons  28346  onaddscl  28347  om2noseqlt  28369  noseqrdgfn  28376  n0fincut  28425  bdayn0sf1o  28440  dfnns2  28442  bdaypw2n0bndlem  28533  bdayfinbndlem1  28537  z12negscl  28548  z12zsodd  28552  z12bdaylem  28554  bdayfinlem  28556  recut  28564  elreno2  28565  brcgr  29047  brbtwn2  29052  axbtwnid  29086  axcontlem7  29117  usgrnloopALT  29350  uhgrspansubgrlem  29437  nbuhgr  29490  nbupgr  29491  wwlksnextprop  30058  elwspths2on  30108  elwspths2onw  30109  erclwwlktr  30170  clwwlknscsh  30210  erclwwlkntr  30219  hashecclwwlkn1  30225  umgrhashecclwwlk  30226  3cyclfrgrrn1  30433  frgrregorufr  30473  frgr2wwlk1  30477  ubthlem1  31019  ubthlem3  31021  htthlem  31066  omlsii  31552  spansncol  31717  nmopun  32163  nmcexi  32175  riesz1  32214  elpjrn  32339  cvcon3  32433  chcv1  32504  atcvatlem  32534  chirredi  32543  br8d  32760  xrge0tsmsd  33214  ordtrest2NEWlem  34180  lmxrge0  34210  esumfsup  34328  esumpcvgval  34336  measdivcstALTV  34483  eulerpartlemgh  34636  dstfrvunirn  34733  afsval  34932  onvf1odlem4  35413  erdszelem8  35512  erdszelem11  35515  erdsze2lem2  35518  connpconn  35549  sconnpi1  35553  cvmsss2  35588  cvmfolem  35593  cvmliftmolem2  35596  cvmliftlem15  35612  cvmlift2lem1  35616  cvmlift3lem4  35636  cvmlift3lem5  35637  satfdmlem  35682  fmla1  35701  gonarlem  35708  gonar  35709  goalrlem  35710  goalr  35711  fmla0disjsuc  35712  fmlasucdisj  35713  satffunlem1lem1  35716  satffunlem1lem2  35717  satffunlem2lem1  35718  mrsub0  35830  mrsubcn  35833  msubrn  35843  msubvrs  35874  br8  36070  br6  36071  br4  36072  cgrtriv  36316  btwntriv2  36326  btwncomim  36327  btwnswapid  36331  btwnintr  36333  btwnexch3  36334  btwnouttr2  36336  ifscgr  36358  cgrxfr  36369  btwnxfr  36370  btwnconn3  36417  segcon2  36419  brsegle  36422  seglecgr12im  36424  broutsideof3  36440  linethru  36467  elhf2  36489  nmulprop  36504  opnregcld  36654  cldregopn  36655  neibastop2lem  36684  tr0elw  36808  tr0el  36809  matunitlindflem1  38079  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem24  38107  poimirlem29  38112  heicant  38118  opnmbllem0  38119  ismblfin  38124  itg2addnclem  38134  itg2addnclem3  38136  itg2gt0cn  38138  ftc1anclem5  38160  ftc2nc  38165  filbcmb  38203  fdc  38208  incsequz  38211  caushft  38224  istotbnd3  38234  equivbnd  38253  cntotbnd  38259  heibor1lem  38272  heibor1  38273  bfplem2  38286  divrngidl  38491  prnc  38530  lshpdisj  39575  cvrcon3b  39865  atnle  39905  hlhgt2  39977  hl0lt1N  39978  hl2at  39993  cvrexchlem  40007  cvratlem  40009  lvolnlelpln  40173  2lplnj  40208  ispsubcl2N  40535  lautcvr  40680  dva1dim  41573  dib1dim  41753  dib1dim2  41756  diclspsn  41782  dih1dimatlem  41917  dihlatat  41925  dihatexv  41926  dihatexv2  41927  lcfrlem9  42138  lcfrlem16  42146  mapdrvallem2  42233  mapd1o  42236  aks6d1c2  42711  elre0re  42834  prjspner1  43172  dffltz  43180  rexlimdv3d  43228  elrfi  43239  isnacs3  43255  eldiophb  43302  eldiophss  43319  diophren  43354  rencldnfilem  43361  pell1234qrdich  43402  pellfundex  43427  lsmfgcl  43615  kercvrlsm  43624  lmhmfgima  43625  lpirlnr  43658  hbtlem2  43665  hbtlem4  43667  hbtlem6  43670  rngunsnply  43710  onexoegt  43785  oaabsb  43835  cantnfresb  43865  omabs2  43873  tfsconcatrev  43889  restuni3  45660  limsupubuz  46251  stoweidlem57  46595  fourierdlem48  46692  fourierdlem49  46693  sge0le  46945  fsetsniunop  47607  cfsetsnfsetfo  47618  fcoresf1  47627  euoreqb  47667  modlt0b  47927  nndivides2  47942  imasetpreimafvbijlemf1  47974  imasetpreimafvbijlemfo  47975  iccpartrn  48000  iccpartiun  48004  iccpartnel  48008  paireqne  48081  reupr  48092  odz2prm2pw  48136  fmtnofac2lem  48141  prmdvdsfmtnof1lem2  48158  2pwp1prm  48162  mod42tp1mod8  48175  lighneallem3  48180  lighneallem4  48183  nprmdvdsfacm1  48197  ppivalnnprm  48198  ppivalnnnprmge6  48199  requad01  48207  requad2  48209  fppr2odd  48317  gbowpos  48345  gbowgt5  48348  gboge9  48350  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  isubgredg  48452  grimcnv  48474  uhgrimedgi  48476  isuspgrim0  48480  isuspgrimlem  48481  gricushgr  48503  clnbgrgrimlem  48519  clnbgrgrim  48520  grimedg  48521  grtrissvtx  48530  stgrusgra  48545  isubgr3stgrlem7  48558  gpgiedgdmellem  48632  gpgusgralem  48642  gpgvtxedg0  48649  gpgvtxedg1  48650  copisnmnd  48755  lidldomn1  48817  affinecomb1  49288  eenglngeehlnmlem2  49324  rrx2vlinest  49327  itsclquadb  49362  aacllem  50386