Theorem rexlimdva 3031

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexlimdvaa  3032  rexlimivv  3036  rexlimdvv  3037  ssexnelpss  3720  ralxfrdOLD  4880  ralxfrd2  4884  otiunsndisj  4980  iunopeqop  4981  elsnxp  5677  foco2  6379  foco2OLD  6380  elunirn  6509  f1elima  6520  tfrlem9a  7482  seqomlem2  7546  oawordexr  7636  odi  7659  oelimcl  7680  nnawordex  7717  nnaordex  7718  oaabs  7724  oaabs2  7725  omabs  7727  ectocld  7814  onfin  8151  dif1en  8193  isfinite2  8218  isfiniteg  8220  fofinf1o  8241  elfiun  8336  suplub2  8367  supisoex  8380  ordtypelem9  8431  ordtypelem10  8432  brwdom2  8478  brwdom3  8487  rankr1ai  8661  fodomfi2  8883  infpwfien  8885  dfac12r  8968  ackbij1  9060  cff1  9080  fin23lem21  9161  isf32lem2  9176  fin1a2lem11  9232  fin1a2lem13  9234  ficard  9387  pwcfsdom  9405  gchina  9521  eltsk2g  9573  tskr1om2  9590  rankcf  9599  inatsk  9600  tskuni  9605  nqereu  9751  ltexnq  9797  1idpr  9851  suplem1pr  9874  supsrlem  9932  axpre-sup  9990  1re  10039  negfi  10971  fiminre  10972  supaddc  10990  supadd  10991  supmul1  10992  supmul  10995  suprzcl2  11778  qmulz  11791  qbtwnre  12030  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  modmuladd  12712  addmodlteq  12745  fsequb  12774  ssnn0fi  12784  hashdom  13168  reuccats1lem  13479  2cshwcshw  13571  wrdl3s3  13705  s3iunsndisj  13707  shftlem  13808  rexuzre  14092  rexico  14093  caubnd  14098  limsupbnd1  14213  limsupbnd2  14214  rlim2lt  14228  rlim3  14229  lo1bdd2  14255  lo1bddrp  14256  o1lo1  14268  climuni  14283  climshftlem  14305  o1co  14317  rlimcn1  14319  climcn1  14322  o1rlimmul  14349  lo1le  14382  rlimno1  14384  isercoll  14398  caurcvg2  14408  serf0  14411  summolem2  14447  zsum  14449  fsum2dlem  14501  geomulcvg  14607  mertenslem2  14617  ntrivcvg  14629  zprod  14667  fprod2dlem  14710  dvds1lem  14993  odd2np1lem  15064  odd2np1  15065  mod2eq1n2dvds  15071  sqoddm1div8z  15078  ltoddhalfle  15085  halfleoddlt  15086  m1expo  15092  flodddiv4  15137  dvdssqim  15273  coprmdvds2  15368  divgcdcoprm0  15379  cncongr1  15381  cncongr2  15382  dvdsnprmd  15403  isprm5  15419  rpexp  15432  ncoprmlnprm  15436  pythagtriplem1  15521  iserodd  15540  pc2dvds  15583  difsqpwdvds  15591  oddprmdvds  15607  prmpwdvds  15608  4sqlem11  15659  vdwapun  15678  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  vdwlem10  15694  vdwnnlem1  15699  vdwnnlem3  15701  0ram  15724  ramub1lem2  15731  ramcl  15733  cshwsiun  15806  cshwrepswhash1  15809  firest  16093  imasvscafn  16197  imasmnd2  17327  dfgrp3lem  17513  imasgrp2  17530  issubg4  17613  gaorber  17741  orbsta  17746  pmtr3ncom  17895  psgnran  17935  odmulg  17973  odbezout  17975  gexdvdsi  17998  sylow1lem3  18015  odcau  18019  sylow2alem1  18032  sylow3lem6  18047  lsmelvalm  18066  efgrelexlemb  18163  efgredeu  18165  cyggeninv  18285  cygctb  18293  cyggexb  18300  dprdssv  18415  dprddisj2  18438  ablfacrplem  18464  pgpfac1lem2  18474  pgpfac1lem5  18478  ringinvnz1ne0  18592  ringinvnzdiv  18593  imasring  18619  dvdsrcl2  18650  dvdsrmul1  18653  lss1d  18963  lssats2  19000  lspsn  19002  lmhmima  19047  lspsneleq  19115  lpiss  19250  mplcoe5lem  19467  mpfind  19536  cply1coe0bi  19670  gsummoncoe1  19674  mpfpf1  19715  pf1mpf  19716  dvdsrzring  19831  znunit  19912  znrrg  19914  cygznlem3  19918  frgpcyg  19922  psgnghm  19926  psgndif  19948  lindfrn  20160  islinds4  20174  mat1dimelbas  20277  mat1dimcrng  20283  scmatdmat  20321  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  smatvscl  20330  cpmatacl  20521  cpmatinvcl  20522  pmatcollpw3fi1lem2  20592  chpscmat  20647  tgcl  20773  clsval2  20854  neindisj  20921  innei  20929  restcld  20976  restcldr  20978  ordtrest2lem  21007  cnprest  21093  lmss  21102  lmcls  21106  lmcnp  21108  isnrm3  21163  isreg2  21181  cmpcovf  21194  cncmp  21195  cmpsub  21203  1stcrest  21256  2ndcrest  21257  dis2ndc  21263  1stccnp  21265  restnlly  21285  cldllycmp  21298  locfincmp  21329  txcnpi  21411  pthaus  21441  txtube  21443  txcmplem1  21444  txcmplem2  21445  txlm  21451  xkohaus  21456  xkococnlem  21462  xkococn  21463  kqfvima  21533  kqreglem1  21544  isfild  21662  fgcl  21682  filuni  21689  isufil2  21712  ufileu  21723  uffix  21725  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  fmco  21765  fclsopn  21818  ufilcmp  21836  cnpfcf  21845  alexsublem  21848  alexsubALT  21855  cldsubg  21914  ghmcnp  21918  qustgpopn  21923  tsmsgsum  21942  tsmsres  21947  tsmsxplem1  21956  tsmsxp  21958  isucn2  22083  ucnprima  22086  imasdsf1olem  22178  blssps  22229  blss  22230  blssexps  22231  blssex  22232  mopni3  22299  blcld  22310  metrest  22329  metcnp3  22345  reperflem  22621  icccmplem3  22627  xrge0tsms  22637  mulc1cncf  22708  cncfco  22710  cnheibor  22754  bndth  22757  lebnumlem3  22762  xlebnum  22764  lebnumii  22765  nmhmcn  22920  cfil3i  23067  cmetcaulem  23086  cfilres  23094  bcthlem4  23124  bcthlem5  23125  ivthlem2  23221  ivthlem3  23222  ivthicc  23227  cniccbdd  23230  ovolunlem1  23265  ovoliunlem2  23271  ovolshftlem2  23278  ovolicc2  23290  iundisj  23316  iunmbl2  23325  dyadmax  23366  opnmbllem  23369  subopnmbl  23372  volivth  23375  vitalilem2  23378  ismbf3d  23421  mbfimaopn2  23424  mbfaddlem  23427  i1fmullem  23461  mbfi1fseqlem4  23485  ellimc3  23643  dvlip  23756  dvlip2  23758  c1liplem1  23759  dvgt0lem1  23765  dvivthlem2  23772  dvne0  23774  lhop1lem  23776  lhop2  23778  lhop  23779  tdeglem4  23820  mdegnn0cl  23831  ply1divex  23896  dvdsq1p  23920  ig1peu  23931  elply2  23952  plypf1  23968  plydivex  24052  aalioulem3  24089  aalioulem5  24091  aaliou  24093  ulmshftlem  24143  ulmcau  24149  ulmss  24151  ulmbdd  24152  ulmcn  24153  radcnvlt1  24172  eflogeq  24348  efopn  24404  cxpeq  24498  angpieqvd  24558  dcubic  24573  xrlimcnp  24695  cxploglim  24704  ftalem2  24800  ftalem7  24805  isppw2  24841  dchrptlem1  24989  dchrptlem3  24991  dchrsum2  24993  lgsdchrval  25079  lgsdchr  25080  gausslemma2dlem1a  25090  lgsquadlem1  25105  2lgslem1c  25118  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  2lgsoddprmlem2  25134  dchrisumlem3  25180  dchrisum0fno1  25200  pntlem3  25298  pntleml  25300  ostth3  25327  brcgr  25780  brbtwn2  25785  axbtwnid  25819  axcontlem7  25850  umgrnloop  26003  usgrnloopALT  26095  uhgrspansubgrlem  26182  nbuhgr  26239  nbupgr  26240  wwlksnextprop  26807  elwspths2on  26853  erclwwlkseqlen  26933  erclwwlkstr  26936  clwwlksnscsh  26940  erclwwlksneqlen  26945  erclwwlksntr  26948  eleclclwwlksn  26953  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  umgr3v3e3cycl  27044  cusconngr  27051  eucrctshift  27103  2pthfrgr  27148  3cyclfrgrrn1  27149  frgrregorufr  27189  frgr2wwlk1  27193  blocnilem  27659  ubthlem1  27726  ubthlem3  27728  htthlem  27774  shsel3  28174  omlsii  28262  spansncol  28427  nmopun  28873  nmcexi  28885  riesz1  28924  elpjrn  29049  cvcon3  29143  chcv1  29214  atcvatlem  29244  chirredi  29253  br8d  29422  iundisjfi  29555  xrge0tsmsd  29785  ordtrest2NEWlem  29968  lmxrge0  29998  indf1ofs  30088  esumcst  30125  esumfsup  30132  esumpcvgval  30140  measdivcstOLD  30287  eulerpartlemgh  30440  dstfrvunirn  30536  afsval  30749  erdszelem8  31180  erdszelem11  31183  erdsze2lem2  31186  connpconn  31217  sconnpi1  31221  cvmsss2  31256  cvmfolem  31261  cvmliftmolem2  31264  cvmliftlem15  31280  cvmlift2lem1  31284  cvmlift3lem4  31304  cvmlift3lem5  31305  mrsub0  31413  mrsubcn  31416  msubrn  31426  msubvrs  31457  dvdspw  31636  br8  31646  br6  31647  br4  31648  trpredtr  31730  frrlem5e  31788  nosupno  31849  nosupbday  31851  scutun12  31917  cgrtriv  32109  btwntriv2  32119  btwncomim  32120  btwnswapid  32124  btwnintr  32126  btwnexch3  32127  btwnouttr2  32129  ifscgr  32151  cgrxfr  32162  btwnxfr  32163  btwnconn3  32210  segcon2  32212  brsegle  32215  brsegle2  32216  seglecgr12im  32217  broutsideof3  32233  linethru  32260  elhf2  32282  opnregcld  32325  cldregopn  32326  neibastop2lem  32355  matunitlindflem1  33405  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  poimirlem29  33438  heicant  33444  opnmbllem0  33445  ismblfin  33450  itg2addnclem  33461  itg2addnclem3  33463  itg2gt0cn  33465  bddiblnc  33480  ftc1anclem5  33489  ftc2nc  33494  filbcmb  33535  sdclem1  33539  fdc  33541  incsequz  33544  caushft  33557  istotbnd3  33570  sstotbnd3  33575  equivbnd  33589  cntotbnd  33595  heibor1lem  33608  heibor1  33609  bfplem2  33622  divrngidl  33827  prnc  33866  prtlem10  34150  lshpdisj  34274  cvrcon3b  34564  atnle  34604  hlhgt2  34675  hl0lt1N  34676  hl2at  34691  cvrexchlem  34705  cvratlem  34707  lvolnlelpln  34871  2lplnj  34906  ispsubcl2N  35233  lautcvr  35378  dva1dim  36273  dib1dim  36454  dib1dim2  36457  diclspsn  36483  dih1dimatlem  36618  dihlatat  36626  dihatexv  36627  dihatexv2  36628  lcfrlem9  36839  lcfrlem16  36847  mapdrvallem2  36934  mapd1o  36937  elrfi  37257  isnacs3  37273  eldiophb  37320  diophrw  37322  eldioph2b  37326  diophin  37336  eldiophss  37338  rexrabdioph  37358  diophren  37377  rencldnfilem  37384  pell1234qrdich  37425  pellfundex  37450  jm2.26a  37567  jm2.27  37575  lsmfgcl  37644  kercvrlsm  37653  lmhmfgima  37654  lpirlnr  37687  hbtlem2  37694  hbtlem4  37696  hbtlem6  37699  rngunsnply  37743  restuni3  39301  suplesup  39555  uzub  39658  limsuppnfdlem  39933  limsuppnflem  39942  limsupubuz  39945  climinf3  39948  limsupre3lem  39964  limsupre3uzlem  39967  limsupvaluz2  39970  supcnvlimsup  39972  stoweidlem57  40274  stoweidlem61  40278  fourierdlem48  40371  fourierdlem49  40372  sge0le  40624  carageniuncllem2  40736  icoresmbl  40757  hspmbllem2  40841  smflimlem2  40980  smfmullem3  41000  smfinflem  41023  otiunsndisjX  41298  iccpartrn  41366  iccpartiun  41370  iccpartnel  41374  reuccatpfxs1lem  41433  reuccatpfxs1  41434  odz2prm2pw  41475  fmtnoprmfac2lem1  41478  fmtnofac2lem  41480  fmtnofac1  41482  prmdvdsfmtnof1lem2  41497  2pwp1prm  41503  mod42tp1mod8  41519  lighneallem2  41523  lighneallem3  41524  lighneallem4  41527  dfodd6  41550  dfeven4  41551  m1expevenALTV  41560  opoeALTV  41594  opeoALTV  41595  gbowpos  41647  gbowgt5  41650  gboge9  41652  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  tgblthelfgottOLD  41709  sprsymrelf1lem  41741  copisnmnd  41809  lidldomn1  41921  uzlidlring  41929  isldepslvec2  42274  m1modmmod  42316  aacllem  42547