Theorem rexlimdva 3130

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 3128	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdvaa  3131  rexlimivv  3171  rexlimdvv  3185  rspceb2dv  3583  ssexnelpss  4069  ralxfrd2  5354  iunopeqop  5468  elsnxp  6243  foco2  7047  elunirn  7191  f1elima  7204  mptcnfimad  7928  releldmdifi  7987  mpoexw  8020  xpord3pred  8092  sexp3  8093  tfrlem9a  8315  seqomlem2  8380  oawordexr  8481  odi  8504  oelimcl  8525  nnawordex  8562  nnaordex  8563  oaabs  8573  oaabs2  8574  omabs  8576  eldifsucnn  8589  coflton  8596  cofon1  8597  cofon2  8598  cofonr  8599  naddunif  8618  ectocld  8716  onfin  9139  dif1ennnALT  9180  isfinite2  9203  isfiniteg  9206  fofinf1o  9241  elfiun  9339  suplub2  9370  supisoex  9384  ordtypelem9  9437  ordtypelem10  9438  brwdom2  9484  brwdom3  9493  ttrcltr  9631  rankr1ai  9713  fodomfi2  9973  infpwfien  9975  dfac12r  10060  ackbij1  10150  cff1  10171  fin23lem21  10252  isf32lem2  10267  fin1a2lem11  10323  fin1a2lem13  10325  ficard  10478  gchina  10612  eltsk2g  10664  tskr1om2  10681  rankcf  10690  inatsk  10691  tskuni  10696  nqereu  10842  ltexnq  10888  1idpr  10942  suplem1pr  10965  supsrlem  11024  axpre-sup  11082  1re  11134  0re  11136  0cnALT  11369  supaddc  12110  supadd  12111  supmul1  12112  supmul  12115  suprzcl2  12857  qmulz  12870  elpq  12894  qbtwnre  13119  ioo0  13291  ico0  13312  ioc0  13313  icc0  13314  addmodlteq  13871  fsequb  13900  hashdom  14304  ccats1alpha  14544  reuccatpfxs1lem  14670  shftlem  14993  rexuzre  15278  rexico  15279  caubnd  15284  limsupbnd1  15407  limsupbnd2  15408  rlim2lt  15422  rlim3  15423  lo1bdd2  15449  lo1bddrp  15450  o1lo1  15462  climuni  15477  climshftlem  15499  o1co  15511  rlimcn1  15513  climcn1  15517  o1rlimmul  15544  lo1le  15577  rlimno1  15579  isercoll  15593  caurcvg2  15603  serf0  15606  summolem2  15641  zsum  15643  fsum2dlem  15695  geomulcvg  15801  mertenslem2  15810  ntrivcvg  15822  zprod  15862  fprod2dlem  15905  dvds1lem  16196  dvdsexp2im  16256  odd2np1lem  16269  sqoddm1div8z  16283  ltoddhalfle  16290  halfleoddlt  16291  flodddiv4  16344  dvdssqim  16483  dvdsexpim  16484  coprmdvds2  16583  divgcdcoprm0  16594  cncongr1  16596  cncongr2  16597  isprm5  16636  rpexp  16651  pythagtriplem1  16746  iserodd  16765  pc2dvds  16809  difsqpwdvds  16817  oddprmdvds  16833  prmpwdvds  16834  4sqlem11  16885  vdwapun  16904  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  vdwlem10  16920  vdwnnlem1  16925  vdwnnlem3  16927  0ram  16950  ramub1lem2  16957  ramcl  16959  cshwsiun  17029  cshwrepswhash1  17032  firest  17354  imasvscafn  17459  imasmnd2  18666  dfgrp3lem  18935  imasgrp2  18952  issubg4  19042  cycsubm  19099  gaorber  19205  orbsta  19210  pmtr3ncom  19372  psgnran  19412  odmulg  19453  odbezout  19455  gexdvdsi  19480  sylow1lem3  19497  odcau  19501  sylow2alem1  19514  sylow3lem6  19529  lsmelvalm  19548  efgrelexlemb  19647  efgredeu  19649  imasabl  19773  cyggeninv  19780  cygctb  19789  cyggexb  19796  dprdssv  19915  dprddisj2  19938  ablfacrplem  19964  pgpfac1lem2  19974  pgpfac1lem5  19978  ringinvnzdiv  20204  imasring  20233  dvdsrcl2  20269  dvdsrmul1  20272  lss1d  20884  lssats2  20921  lspsn  20923  lmhmima  20969  ring2idlqusb  21235  rngqiprngfulem2  21237  lpiss  21254  dvdsrzring  21386  pzriprnglem5  21410  pzriprnglem8  21413  pzriprnglem10  21415  pzriprnglem11  21416  znunit  21488  znrrg  21490  cygznlem3  21494  frgpcyg  21498  lindfrn  21746  mplcoe5lem  21962  mpfind  22030  gsummoncoe1  22211  mpfpf1  22254  pf1mpf  22255  mat1dimelbas  22374  scmatdmat  22418  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  cpmatacl  22619  chpscmat  22745  tgcl  22872  clsval2  22953  innei  23028  restcld  23075  restcldr  23077  ordtrest2lem  23106  cnprest  23192  lmss  23201  lmcls  23205  lmcnp  23207  isreg2  23280  cmpcovf  23294  cncmp  23295  cmpsub  23303  1stcrest  23356  2ndcrest  23357  1stccnp  23365  restnlly  23385  cldllycmp  23398  locfincmp  23429  txcnpi  23511  pthaus  23541  txtube  23543  txcmplem1  23544  txcmplem2  23545  txlm  23551  xkohaus  23556  xkococnlem  23562  xkococn  23563  kqfvima  23633  kqreglem1  23644  isfild  23761  filuni  23788  isufil2  23811  uffix  23824  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  fmfnfm  23861  fmco  23864  fclsopn  23917  ufilcmp  23935  cnpfcf  23944  alexsublem  23947  alexsubALT  23954  cldsubg  24014  ghmcnp  24018  qustgpopn  24023  tsmsgsum  24042  tsmsres  24047  tsmsxplem1  24056  tsmsxp  24058  isucn2  24182  ucnprima  24185  imasdsf1olem  24277  blssps  24328  blss  24329  blssexps  24330  blssex  24331  mopni3  24398  blcld  24409  metrest  24428  metcnp3  24444  reperflem  24723  icccmplem3  24729  xrge0tsms  24739  mulc1cncf  24814  cncfco  24816  cnheibor  24870  bndth  24873  lebnumlem3  24878  xlebnum  24880  lebnumii  24881  nmhmcn  25036  cfil3i  25185  cmetcaulem  25204  cfilres  25212  bcthlem4  25243  ivthlem2  25369  ivthlem3  25370  ivthicc  25375  cniccbdd  25378  ovolunlem1  25414  ovoliunlem2  25420  ovolshftlem2  25427  ovolicc2  25439  iunmbl2  25474  dyadmax  25515  opnmbllem  25518  subopnmbl  25521  volivth  25524  ismbf3d  25571  mbfimaopn2  25574  mbfaddlem  25577  i1fmullem  25611  mbfi1fseqlem4  25635  bddiblnc  25759  ellimc3  25796  dvlip  25914  dvlip2  25916  c1liplem1  25917  dvgt0lem1  25923  dvivthlem2  25930  dvne0  25932  lhop1lem  25934  lhop2  25936  lhop  25937  tdeglem4  25981  mdegnn0cl  25992  ply1divex  26058  dvdsq1p  26084  ig1peu  26096  elply2  26117  plypf1  26133  plydivex  26221  aalioulem3  26258  aalioulem5  26260  aaliou  26262  ulmshftlem  26314  ulmcau  26320  ulmss  26322  ulmbdd  26323  ulmcn  26324  radcnvlt1  26343  eflogeq  26527  efopn  26583  cxpeq  26683  angpieqvd  26757  xrlimcnp  26894  cxploglim  26904  ftalem2  27000  ftalem7  27005  isppw2  27041  dchrptlem1  27191  dchrptlem3  27193  dchrsum2  27195  lgsdchrval  27281  lgsdchr  27282  gausslemma2dlem1a  27292  lgsquadlem1  27307  2lgsoddprmlem2  27336  dchrisumlem3  27418  dchrisum0fno1  27438  pntlem3  27536  pntleml  27538  ostth3  27565  nosupno  27631  nosupbday  27633  noinfbday  27648  scutun12  27739  oldssmade  27809  addsproplem2  27900  addsuniflem  27931  addsbdaylem  27946  negsid  27970  negsunif  27984  precsexlem6  28137  precsexlem7  28138  precsexlem11  28142  bdayon  28196  onaddscl  28197  om2noseqlt  28216  noseqrdgfn  28223  n0sfincut  28269  bdayn0sf1o  28282  dfnns2  28284  zs12negscl  28373  zs12zodd  28377  zs12bday  28379  recut  28383  brcgr  28863  brbtwn2  28868  axbtwnid  28902  axcontlem7  28933  usgrnloopALT  29166  uhgrspansubgrlem  29253  nbuhgr  29306  nbupgr  29307  wwlksnextprop  29875  elwspths2on  29923  erclwwlktr  29984  clwwlknscsh  30024  erclwwlkntr  30033  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  3cyclfrgrrn1  30247  frgrregorufr  30287  frgr2wwlk1  30291  ubthlem1  30832  ubthlem3  30834  htthlem  30879  omlsii  31365  spansncol  31530  nmopun  31976  nmcexi  31988  riesz1  32027  elpjrn  32152  cvcon3  32246  chcv1  32317  atcvatlem  32347  chirredi  32356  br8d  32571  xrge0tsmsd  33028  ordtrest2NEWlem  33888  lmxrge0  33918  esumfsup  34036  esumpcvgval  34044  measdivcstALTV  34191  eulerpartlemgh  34345  dstfrvunirn  34442  afsval  34638  onvf1odlem4  35078  erdszelem8  35170  erdszelem11  35173  erdsze2lem2  35176  connpconn  35207  sconnpi1  35211  cvmsss2  35246  cvmfolem  35251  cvmliftmolem2  35254  cvmliftlem15  35270  cvmlift2lem1  35274  cvmlift3lem4  35294  cvmlift3lem5  35295  satfdmlem  35340  fmla1  35359  gonarlem  35366  gonar  35367  goalrlem  35368  goalr  35369  fmla0disjsuc  35370  fmlasucdisj  35371  satffunlem1lem1  35374  satffunlem1lem2  35375  satffunlem2lem1  35376  mrsub0  35488  mrsubcn  35491  msubrn  35501  msubvrs  35532  br8  35728  br6  35729  br4  35730  cgrtriv  35975  btwntriv2  35985  btwncomim  35986  btwnswapid  35990  btwnintr  35992  btwnexch3  35993  btwnouttr2  35995  ifscgr  36017  cgrxfr  36028  btwnxfr  36029  btwnconn3  36076  segcon2  36078  brsegle  36081  seglecgr12im  36083  broutsideof3  36099  linethru  36126  elhf2  36148  opnregcld  36303  cldregopn  36304  neibastop2lem  36333  matunitlindflem1  37595  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem24  37623  poimirlem29  37628  heicant  37634  opnmbllem0  37635  ismblfin  37640  itg2addnclem  37650  itg2addnclem3  37652  itg2gt0cn  37654  ftc1anclem5  37676  ftc2nc  37681  filbcmb  37719  fdc  37724  incsequz  37727  caushft  37740  istotbnd3  37750  equivbnd  37769  cntotbnd  37775  heibor1lem  37788  heibor1  37789  bfplem2  37802  divrngidl  38007  prnc  38046  lshpdisj  38965  cvrcon3b  39255  atnle  39295  hlhgt2  39368  hl0lt1N  39369  hl2at  39384  cvrexchlem  39398  cvratlem  39400  lvolnlelpln  39564  2lplnj  39599  ispsubcl2N  39926  lautcvr  40071  dva1dim  40964  dib1dim  41144  dib1dim2  41147  diclspsn  41173  dih1dimatlem  41308  dihlatat  41316  dihatexv  41317  dihatexv2  41318  lcfrlem9  41529  lcfrlem16  41537  mapdrvallem2  41624  mapd1o  41627  aks6d1c2  42103  elre0re  42227  prjspner1  42599  dffltz  42607  rexlimdv3d  42656  elrfi  42667  isnacs3  42683  eldiophb  42730  eldiophss  42747  diophren  42786  rencldnfilem  42793  pell1234qrdich  42834  pellfundex  42859  lsmfgcl  43047  kercvrlsm  43056  lmhmfgima  43057  lpirlnr  43090  hbtlem2  43097  hbtlem4  43099  hbtlem6  43102  rngunsnply  43142  onexoegt  43217  oaabsb  43267  cantnfresb  43297  omabs2  43305  tfsconcatrev  43321  restuni3  45096  limsupubuz  45695  stoweidlem57  46039  fourierdlem48  46136  fourierdlem49  46137  sge0le  46389  fsetsniunop  47034  cfsetsnfsetfo  47045  fcoresf1  47054  euoreqb  47094  modlt0b  47348  imasetpreimafvbijlemf1  47389  imasetpreimafvbijlemfo  47390  iccpartrn  47415  iccpartiun  47419  iccpartnel  47423  paireqne  47496  reupr  47507  odz2prm2pw  47548  fmtnofac2lem  47553  prmdvdsfmtnof1lem2  47570  2pwp1prm  47574  mod42tp1mod8  47587  lighneallem3  47592  lighneallem4  47595  requad01  47606  requad2  47608  fppr2odd  47716  gbowpos  47744  gbowgt5  47747  gboge9  47749  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  isubgredg  47851  grimcnv  47873  uhgrimedgi  47875  isuspgrim0  47879  isuspgrimlem  47880  gricushgr  47902  clnbgrgrimlem  47918  clnbgrgrim  47919  grimedg  47920  grtrissvtx  47929  stgrusgra  47944  isubgr3stgrlem7  47957  gpgiedgdmellem  48031  gpgusgralem  48041  gpgvtxedg0  48048  gpgvtxedg1  48049  copisnmnd  48154  lidldomn1  48216  affinecomb1  48688  eenglngeehlnmlem2  48724  rrx2vlinest  48727  itsclquadb  48762  aacllem  49787