Theorem rexlimdva 3164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  rexlimdvaa  3165  rexlimivv  3205  rexlimdvv  3219  rspceb2dv  3581  ssexnelpss  4065  ralxfrd2  5374  iunopeqop  5494  iunopeqopOLD  5495  elsnxp  6287  foco2  7101  elunirn  7247  f1elima  7259  mptcnfimad  7987  releldmdifi  8045  mpoexw  8080  xpord3pred  8153  sexp3  8154  tfrlem9a  8378  seqomlem2  8445  oawordexr  8548  odi  8571  oelimcl  8593  nnawordex  8630  nnaordex  8631  oaabs  8641  oaabs2  8642  omabs  8644  eldifsucnn  8657  coflton  8664  cofon1  8665  cofon2  8666  cofonr  8667  naddunif  8687  ectocld  8787  onfin  9214  dif1ennnALT  9252  isfinite2  9274  isfiniteg  9276  fofinf1o  9305  elfiun  9406  suplub2  9437  supisoex  9451  ordtypelem9  9504  ordtypelem10  9505  brwdom2  9551  brwdom3  9560  ttrcltr  9701  rankr1ai  9788  elhf2  9891  fodomfi2  10120  infpwfien  10122  dfac12r  10206  ackbij1  10296  cff1  10317  fin23lem21  10398  isf32lem2  10413  fin1a2lem11  10469  fin1a2lem13  10471  ficard  10630  gchina  10765  eltsk2g  10817  tskhf  10834  rankcf  10843  inatsk  10844  tskuni  10849  nqereu  10995  ltexnq  11041  1idpr  11095  suplem1pr  11118  supsrlem  11177  axpre-sup  11235  1re  11289  0re  11291  0cnALT  11526  supaddc  12265  supadd  12266  supmul1  12267  supmul  12270  suprzcl2  13046  qmulz  13059  elpq  13084  qbtwnre  13310  ioo0  13482  ico0  13503  ioc0  13504  icc0  13505  addmodlteq  14069  fsequb  14098  hashdom  14503  ccats1alpha  14747  reuccatpfxs1lem  14875  shftlem  15201  rexuzre  15500  rexico  15501  caubnd  15506  limsupbnd1  15629  limsupbnd2  15630  rlim2lt  15644  rlim3  15645  lo1bdd2  15671  lo1bddrp  15672  o1lo1  15684  climuni  15699  climshftlem  15721  o1co  15733  rlimcn1  15735  climcn1  15739  o1rlimmul  15766  lo1le  15799  rlimno1  15801  isercoll  15815  caurcvg2  15825  serf0  15828  summolem2  15862  zsum  15864  fsum2dlem  15916  geomulcvg  16025  mertenslem2  16034  ntrivcvg  16046  zprod  16084  fprod2dlem  16127  dvds1lem  16417  dvdsexp2im  16477  odd2np1lem  16490  sqoddm1div8z  16504  ltoddhalfle  16511  halfleoddlt  16512  flodddiv4  16565  dvdssqim  16707  dvdsexpim  16708  coprmdvds2  16809  divgcdcoprm0  16820  cncongr1  16822  cncongr2  16823  isprm5  16863  rpexp  16878  pythagtriplem1  16974  iserodd  16993  pc2dvds  17037  difsqpwdvds  17045  oddprmdvds  17061  prmpwdvds  17062  4sqlem11  17113  vdwapun  17132  vdwlem2  17140  vdwlem6  17144  vdwlem8  17146  vdwlem10  17148  vdwnnlem1  17153  vdwnnlem3  17155  0ram  17178  ramub1lem2  17185  ramcl  17187  cshwsiun  17257  cshwrepswhash1  17260  firest  17583  imasvscafn  17689  imasmgm2  18843  imasmnd2  18948  dfgrp3lem  19228  imasgrp2  19245  issubg4  19336  cycsubm  19397  gaorber  19502  orbsta  19507  pmtr3ncom  19669  psgnran  19709  odmulg  19750  odbezout  19752  gexdvdsi  19777  sylow1lem3  19794  odcau  19798  sylow2alem1  19811  sylow3lem6  19826  lsmelvalm  19845  efgrelexlemb  19944  efgredeu  19946  imasabl  20070  cyggeninv  20077  cygctb  20086  cyggexb  20093  dprdssv  20212  dprddisj2  20235  ablfacrplem  20261  pgpfac1lem2  20271  pgpfac1lem5  20275  ringinvnzdiv  20512  imasring  20540  dvdsrcl2  20576  dvdsrmul1  20579  lss1d  21218  lssats2  21255  lspsn  21257  lmhmima  21302  rspsn0  21506  ring2idlqusb  21586  rngqiprngfulem2  21588  lpiss  21633  dvdsrzring  21747  pzriprnglem5  21771  pzriprnglem8  21774  pzriprnglem10  21776  pzriprnglem11  21777  znunit  21849  znrrg  21851  cygznlem3  21855  frgpcyg  21859  lindfrn  22107  mplcoe5lem  22328  mpfind  22404  gsummoncoe1  22606  mpfpf1  22649  pf1mpf  22650  mat1dimelbas  22766  scmatdmat  22810  scmataddcl  22811  scmatsubcl  22812  scmatmulcl  22813  matunitlindflem1  22974  cpmatacl  23014  chpscmat  23140  tgcl  23267  clsval2  23348  innei  23423  restcld  23470  restcldr  23472  ordtrest2lem  23501  cnprest  23587  lmss  23596  lmcls  23600  lmcnp  23602  isreg2  23675  cmpcovf  23689  cncmp  23690  cmpsub  23698  1stcrest  23751  2ndcrest  23752  1stccnp  23761  restnlly  23781  cldllycmp  23794  locfincmp  23825  txcnpi  23907  pthaus  23937  txtube  23939  txcmplem1  23940  txcmplem2  23941  txlm  23947  xkohaus  23952  xkococnlem  23958  xkococn  23959  kqfvima  24029  kqreglem1  24040  isfild  24157  filuni  24184  isufil2  24207  uffix  24220  rnelfm  24252  fmfnfmlem2  24254  fmfnfmlem4  24256  fmfnfm  24257  fmco  24260  fclsopn  24313  ufilcmp  24331  cnpfcf  24340  alexsublem  24343  alexsubALT  24350  cldsubg  24410  ghmcnp  24414  qustgpopn  24419  tsmsgsum  24438  tsmsres  24443  tsmsxplem1  24452  tsmsxp  24454  isucn2  24577  ucnprima  24580  imasdsf1olem  24672  blssps  24723  blss  24724  blssexps  24725  blssex  24726  mopni3  24793  blcld  24804  metrest  24823  metcnp3  24839  reperflem  25118  icccmplem3  25124  xrge0tsms  25134  mulc1cncf  25206  cncfco  25208  cnheibor  25256  bndth  25259  lebnumlem3  25264  xlebnum  25266  lebnumii  25267  nmhmcn  25421  cfil3i  25570  cmetcaulem  25589  cfilres  25597  bcthlem4  25628  ivthlem2  25753  ivthlem3  25754  ivthicc  25759  cniccbdd  25762  ovolunlem1  25798  ovoliunlem2  25804  ovolshftlem2  25811  ovolicc2  25823  iunmbl2  25858  dyadmax  25899  opnmbllem  25902  subopnmbl  25905  volivth  25908  ismbf3d  25955  mbfimaopn2  25958  mbfaddlem  25961  i1fmullem  25995  mbfi1fseqlem4  26019  bddiblnc  26142  ellimc3  26179  dvlip  26293  dvlip2  26295  c1liplem1  26296  dvgt0lem1  26302  dvivthlem2  26309  dvne0  26311  lhop1lem  26313  lhop2  26315  lhop  26316  tdeglem4  26358  mdegnn0cl  26369  ply1divex  26435  dvdsq1p  26461  ig1peu  26473  elply2  26494  plypf1  26511  plydivex  26600  aalioulem3  26643  aalioulem5  26645  aaliou  26647  ulmshftlem  26698  ulmcau  26704  ulmss  26706  ulmbdd  26707  ulmcn  26708  radcnvlt1  26727  eflogeq  26912  efopn  26968  cxpeq  27067  angpieqvd  27141  xrlimcnp  27278  cxploglim  27287  ftalem2  27383  ftalem7  27388  isppw2  27424  dchrptlem1  27573  dchrptlem3  27575  dchrsum2  27577  lgsdchrval  27663  lgsdchr  27664  gausslemma2dlem1a  27674  lgsquadlem1  27689  2lgsoddprmlem2  27718  dchrisumlem3  27800  dchrisum0fno1  27820  pntlem3  27918  pntleml  27920  ostth3  27947  fltoprm  27977  nosupno  28042  nosupbday  28044  noinfbday  28059  cutsun12  28158  oldssmade  28235  addsproplem2  28338  addsuniflem  28369  addbdaylem  28385  negsid  28409  negsunif  28423  negleft  28426  negright  28427  precsexlem6  28580  precsexlem7  28581  precsexlem11  28585  bdayons  28644  onaddscl  28645  om2noseqlt  28667  noseqrdgfn  28674  n0fincut  28723  bdayn0sf1o  28738  dfnns2  28740  bdaypw2n0bndlem  28831  bdayfinbndlem1  28835  z12negscl  28846  z12zsodd  28850  z12bdaylem  28852  bdayfinlem  28854  recut  28862  elreno2  28863  brcgr  29460  brbtwn2  29465  axbtwnid  29499  axcontlem7  29530  usgrnloopALT  29766  uhgrspansubgrlem  29853  nbuhgr  29906  nbupgr  29907  wwlksnextprop  30483  elwspths2on  30533  elwspths2onw  30534  erclwwlktr  30595  clwwlknscsh  30635  erclwwlkntr  30644  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  3cyclfrgrrn1  30868  frgrregorufr  30908  frgr2wwlk1  30912  ubthlem1  31454  ubthlem3  31456  htthlem  31501  omlsii  31987  spansncol  32152  nmopun  32598  nmcexi  32610  riesz1  32649  elpjrn  32774  cvcon3  32868  chcv1  32939  atcvatlem  32969  chirredi  32978  br8d  33184  xrge0tsmsd  33616  ordtrest2NEWlem  34536  lmxrge0  34566  esumfsup  34684  esumpcvgval  34692  measdivcstALTV  34840  eulerpartlemgh  34993  dstfrvunirn  35090  afsval  35286  onvf1odlem4  35858  erdszelem8  35932  erdszelem11  35935  erdsze2lem2  35938  connpconn  35969  sconnpi1  35973  cvmsss2  36008  cvmfolem  36013  cvmliftmolem2  36016  cvmliftlem15  36032  cvmlift2lem1  36036  cvmlift3lem4  36056  cvmlift3lem5  36057  satfdmlem  36102  fmla1  36121  gonarlem  36128  gonar  36129  goalrlem  36130  goalr  36131  fmla0disjsuc  36132  fmlasucdisj  36133  satffunlem1lem1  36136  satffunlem1lem2  36137  satffunlem2lem1  36138  mrsub0  36250  mrsubcn  36253  msubrn  36263  msubvrs  36294  br8  36490  br6  36491  br4  36492  cgrtriv  36737  btwntriv2  36747  btwncomim  36748  btwnswapid  36752  btwnintr  36754  btwnexch3  36755  btwnouttr2  36757  ifscgr  36779  cgrxfr  36790  btwnxfr  36791  btwnconn3  36838  segcon2  36840  brsegle  36843  seglecgr12im  36845  broutsideof3  36861  linethru  36888  nmulprop  36909  opnregcld  37088  cldregopn  37089  neibastop2lem  37118  tr0elw  37242  tr0el  37243  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem24  38530  poimirlem29  38535  heicant  38541  opnmbllem0  38542  ismblfin  38547  itg2addnclem  38557  itg2addnclem3  38559  itg2gt0cn  38561  ftc1anclem5  38583  ftc2nc  38588  filbcmb  38642  fdc  38647  incsequz  38650  caushft  38663  istotbnd3  38673  equivbnd  38692  cntotbnd  38698  heibor1lem  38711  heibor1  38712  bfplem2  38725  divrngidl  38930  prnc  38969  lshpdisj  40012  cvrcon3b  40302  atnle  40342  hlhgt2  40414  hl0lt1N  40415  hl2at  40430  cvrexchlem  40444  cvratlem  40446  lvolnlelpln  40610  2lplnj  40645  ispsubcl2N  40972  lautcvr  41117  dva1dim  42010  dib1dim  42190  dib1dim2  42193  diclspsn  42219  dih1dimatlem  42354  dihlatat  42362  dihatexv  42363  dihatexv2  42364  lcfrlem9  42575  lcfrlem16  42583  mapdrvallem2  42670  mapd1o  42673  aks6d1c2  43148  elre0re  43273  prjspner1  43616  dffltz  43624  rexlimdv3d  43647  elrfi  43658  isnacs3  43674  eldiophb  43721  eldiophss  43738  diophren  43773  rencldnfilem  43780  pell1234qrdich  43821  pellfundex  43846  lsmfgcl  44034  kercvrlsm  44043  lmhmfgima  44044  lpirlnr  44077  hbtlem2  44084  hbtlem4  44086  hbtlem6  44089  rngunsnply  44129  onexoegt  44204  oaabsb  44254  cantnfresb  44284  omabs2  44292  tfsconcatrev  44308  restuni3  46076  limsupubuz  46667  stoweidlem57  47011  fourierdlem48  47108  fourierdlem49  47109  sge0le  47361  fsetsniunop  48063  cfsetsnfsetfo  48074  fcoresf1  48083  euoreqb  48123  modlt0b  48383  nndivides2  48398  imasetpreimafvbijlemf1  48430  imasetpreimafvbijlemfo  48431  iccpartrn  48456  iccpartiun  48460  iccpartnel  48464  paireqne  48537  reupr  48548  odz2prm2pw  48592  fmtnofac2lem  48597  prmdvdsfmtnof1lem2  48614  2pwp1prm  48618  mod42tp1mod8  48631  lighneallem3  48636  lighneallem4  48639  nprmdvdsfacm1  48653  ppivalnnprm  48654  ppivalnnnprmge6  48655  requad01  48663  requad2  48665  fppr2odd  48773  gbowpos  48801  gbowgt5  48804  gboge9  48806  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  isubgredg  48908  grimcnv  48930  uhgrimedgi  48932  isuspgrim0  48936  isuspgrimlem  48937  gricushgr  48959  clnbgrgrimlem  48975  clnbgrgrim  48976  grimedg  48977  grtrissvtx  48986  stgrusgra  49001  isubgr3stgrlem7  49014  gpgiedgdmellem  49088  gpgusgralem  49098  gpgvtxedg0  49105  gpgvtxedg1  49106  copisnmnd  49210  lidldomn1  49272  affinecomb1  49758  eenglngeehlnmlem2  49794  rrx2vlinest  49797  itsclquadb  49832  aacllem  50883