Theorem rexlimdva 3138

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

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 3062

This theorem is referenced by:  rexlimdvaa  3139  rexlimivv  3179  rexlimdvv  3193  rspceb2dv  3568  ssexnelpss  4056  ralxfrd2  5354  iunopeqop  5475  iunopeqopOLD  5476  elsnxp  6255  foco2  7061  elunirn  7206  f1elima  7218  mptcnfimad  7939  releldmdifi  7998  mpoexw  8031  xpord3pred  8102  sexp3  8103  tfrlem9a  8325  seqomlem2  8390  oawordexr  8491  odi  8514  oelimcl  8536  nnawordex  8573  nnaordex  8574  oaabs  8584  oaabs2  8585  omabs  8587  eldifsucnn  8600  coflton  8607  cofon1  8608  cofon2  8609  cofonr  8610  naddunif  8629  ectocld  8729  onfin  9149  dif1ennnALT  9187  isfinite2  9208  isfiniteg  9210  fofinf1o  9242  elfiun  9343  suplub2  9374  supisoex  9388  ordtypelem9  9441  ordtypelem10  9442  brwdom2  9488  brwdom3  9497  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  11381  supaddc  12123  supadd  12124  supmul1  12125  supmul  12128  suprzcl2  12888  qmulz  12901  elpq  12925  qbtwnre  13151  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  addmodlteq  13908  fsequb  13937  hashdom  14341  ccats1alpha  14582  reuccatpfxs1lem  14708  shftlem  15030  rexuzre  15315  rexico  15316  caubnd  15321  limsupbnd1  15444  limsupbnd2  15445  rlim2lt  15459  rlim3  15460  lo1bdd2  15486  lo1bddrp  15487  o1lo1  15499  climuni  15514  climshftlem  15536  o1co  15548  rlimcn1  15550  climcn1  15554  o1rlimmul  15581  lo1le  15614  rlimno1  15616  isercoll  15630  caurcvg2  15640  serf0  15643  summolem2  15678  zsum  15680  fsum2dlem  15732  geomulcvg  15841  mertenslem2  15850  ntrivcvg  15862  zprod  15902  fprod2dlem  15945  dvds1lem  16236  dvdsexp2im  16296  odd2np1lem  16309  sqoddm1div8z  16323  ltoddhalfle  16330  halfleoddlt  16331  flodddiv4  16384  dvdssqim  16523  dvdsexpim  16524  coprmdvds2  16623  divgcdcoprm0  16634  cncongr1  16636  cncongr2  16637  isprm5  16677  rpexp  16692  pythagtriplem1  16787  iserodd  16806  pc2dvds  16850  difsqpwdvds  16858  oddprmdvds  16874  prmpwdvds  16875  4sqlem11  16926  vdwapun  16945  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  vdwnnlem1  16966  vdwnnlem3  16968  0ram  16991  ramub1lem2  16998  ramcl  17000  cshwsiun  17070  cshwrepswhash1  17073  firest  17395  imasvscafn  17501  imasmnd2  18742  dfgrp3lem  19014  imasgrp2  19031  issubg4  19121  cycsubm  19177  gaorber  19283  orbsta  19288  pmtr3ncom  19450  psgnran  19490  odmulg  19531  odbezout  19533  gexdvdsi  19558  sylow1lem3  19575  odcau  19579  sylow2alem1  19592  sylow3lem6  19607  lsmelvalm  19626  efgrelexlemb  19725  efgredeu  19727  imasabl  19851  cyggeninv  19858  cygctb  19867  cyggexb  19874  dprdssv  19993  dprddisj2  20016  ablfacrplem  20042  pgpfac1lem2  20052  pgpfac1lem5  20056  ringinvnzdiv  20282  imasring  20310  dvdsrcl2  20346  dvdsrmul1  20349  lss1d  20958  lssats2  20995  lspsn  20997  lmhmima  21042  ring2idlqusb  21308  rngqiprngfulem2  21310  lpiss  21327  dvdsrzring  21441  pzriprnglem5  21465  pzriprnglem8  21468  pzriprnglem10  21470  pzriprnglem11  21471  znunit  21543  znrrg  21545  cygznlem3  21549  frgpcyg  21553  lindfrn  21801  mplcoe5lem  22017  mpfind  22093  gsummoncoe1  22273  mpfpf1  22316  pf1mpf  22317  mat1dimelbas  22436  scmatdmat  22480  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  cpmatacl  22681  chpscmat  22807  tgcl  22934  clsval2  23015  innei  23090  restcld  23137  restcldr  23139  ordtrest2lem  23168  cnprest  23254  lmss  23263  lmcls  23267  lmcnp  23269  isreg2  23342  cmpcovf  23356  cncmp  23357  cmpsub  23365  1stcrest  23418  2ndcrest  23419  1stccnp  23427  restnlly  23447  cldllycmp  23460  locfincmp  23491  txcnpi  23573  pthaus  23603  txtube  23605  txcmplem1  23606  txcmplem2  23607  txlm  23613  xkohaus  23618  xkococnlem  23624  xkococn  23625  kqfvima  23695  kqreglem1  23706  isfild  23823  filuni  23850  isufil2  23873  uffix  23886  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  fmfnfm  23923  fmco  23926  fclsopn  23979  ufilcmp  23997  cnpfcf  24006  alexsublem  24009  alexsubALT  24016  cldsubg  24076  ghmcnp  24080  qustgpopn  24085  tsmsgsum  24104  tsmsres  24109  tsmsxplem1  24118  tsmsxp  24120  isucn2  24243  ucnprima  24246  imasdsf1olem  24338  blssps  24389  blss  24390  blssexps  24391  blssex  24392  mopni3  24459  blcld  24470  metrest  24489  metcnp3  24505  reperflem  24784  icccmplem3  24790  xrge0tsms  24800  mulc1cncf  24872  cncfco  24874  cnheibor  24922  bndth  24925  lebnumlem3  24930  xlebnum  24932  lebnumii  24933  nmhmcn  25087  cfil3i  25236  cmetcaulem  25255  cfilres  25263  bcthlem4  25294  ivthlem2  25419  ivthlem3  25420  ivthicc  25425  cniccbdd  25428  ovolunlem1  25464  ovoliunlem2  25470  ovolshftlem2  25477  ovolicc2  25489  iunmbl2  25524  dyadmax  25565  opnmbllem  25568  subopnmbl  25571  volivth  25574  ismbf3d  25621  mbfimaopn2  25624  mbfaddlem  25627  i1fmullem  25661  mbfi1fseqlem4  25685  bddiblnc  25809  ellimc3  25846  dvlip  25960  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  dvivthlem2  25976  dvne0  25978  lhop1lem  25980  lhop2  25982  lhop  25983  tdeglem4  26025  mdegnn0cl  26036  ply1divex  26102  dvdsq1p  26128  ig1peu  26140  elply2  26161  plypf1  26177  plydivex  26263  aalioulem3  26300  aalioulem5  26302  aaliou  26304  ulmshftlem  26354  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  radcnvlt1  26383  eflogeq  26566  efopn  26622  cxpeq  26721  angpieqvd  26795  xrlimcnp  26932  cxploglim  26941  ftalem2  27037  ftalem7  27042  isppw2  27078  dchrptlem1  27227  dchrptlem3  27229  dchrsum2  27231  lgsdchrval  27317  lgsdchr  27318  gausslemma2dlem1a  27328  lgsquadlem1  27343  2lgsoddprmlem2  27372  dchrisumlem3  27454  dchrisum0fno1  27474  pntlem3  27572  pntleml  27574  ostth3  27601  nosupno  27667  nosupbday  27669  noinfbday  27684  cutsun12  27782  oldssmade  27859  addsproplem2  27962  addsuniflem  27993  addbdaylem  28009  negsid  28033  negsunif  28047  negleft  28050  negright  28051  precsexlem6  28204  precsexlem7  28205  precsexlem11  28209  bdayons  28268  onaddscl  28269  om2noseqlt  28291  noseqrdgfn  28298  n0fincut  28347  bdayn0sf1o  28362  dfnns2  28364  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  z12negscl  28470  z12zsodd  28474  z12bdaylem  28476  bdayfinlem  28478  recut  28486  elreno2  28487  brcgr  28969  brbtwn2  28974  axbtwnid  29008  axcontlem7  29039  usgrnloopALT  29272  uhgrspansubgrlem  29359  nbuhgr  29412  nbupgr  29413  wwlksnextprop  29980  elwspths2on  30030  elwspths2onw  30031  erclwwlktr  30092  clwwlknscsh  30132  erclwwlkntr  30141  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  3cyclfrgrrn1  30355  frgrregorufr  30395  frgr2wwlk1  30399  ubthlem1  30941  ubthlem3  30943  htthlem  30988  omlsii  31474  spansncol  31639  nmopun  32085  nmcexi  32097  riesz1  32136  elpjrn  32261  cvcon3  32355  chcv1  32426  atcvatlem  32456  chirredi  32465  br8d  32681  xrge0tsmsd  33134  ordtrest2NEWlem  34066  lmxrge0  34096  esumfsup  34214  esumpcvgval  34222  measdivcstALTV  34369  eulerpartlemgh  34522  dstfrvunirn  34619  afsval  34815  onvf1odlem4  35288  erdszelem8  35380  erdszelem11  35383  erdsze2lem2  35386  connpconn  35417  sconnpi1  35421  cvmsss2  35456  cvmfolem  35461  cvmliftmolem2  35464  cvmliftlem15  35480  cvmlift2lem1  35484  cvmlift3lem4  35504  cvmlift3lem5  35505  satfdmlem  35550  fmla1  35569  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  fmla0disjsuc  35580  fmlasucdisj  35581  satffunlem1lem1  35584  satffunlem1lem2  35585  satffunlem2lem1  35586  mrsub0  35698  mrsubcn  35701  msubrn  35711  msubvrs  35742  br8  35938  br6  35939  br4  35940  cgrtriv  36184  btwntriv2  36194  btwncomim  36195  btwnswapid  36199  btwnintr  36201  btwnexch3  36202  btwnouttr2  36204  ifscgr  36226  cgrxfr  36237  btwnxfr  36238  btwnconn3  36285  segcon2  36287  brsegle  36290  seglecgr12im  36292  broutsideof3  36308  linethru  36335  elhf2  36357  opnregcld  36512  cldregopn  36513  neibastop2lem  36542  tr0elw  36666  tr0el  36667  matunitlindflem1  37937  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  poimirlem29  37970  heicant  37976  opnmbllem0  37977  ismblfin  37982  itg2addnclem  37992  itg2addnclem3  37994  itg2gt0cn  37996  ftc1anclem5  38018  ftc2nc  38023  filbcmb  38061  fdc  38066  incsequz  38069  caushft  38082  istotbnd3  38092  equivbnd  38111  cntotbnd  38117  heibor1lem  38130  heibor1  38131  bfplem2  38144  divrngidl  38349  prnc  38388  lshpdisj  39433  cvrcon3b  39723  atnle  39763  hlhgt2  39835  hl0lt1N  39836  hl2at  39851  cvrexchlem  39865  cvratlem  39867  lvolnlelpln  40031  2lplnj  40066  ispsubcl2N  40393  lautcvr  40538  dva1dim  41431  dib1dim  41611  dib1dim2  41614  diclspsn  41640  dih1dimatlem  41775  dihlatat  41783  dihatexv  41784  dihatexv2  41785  lcfrlem9  41996  lcfrlem16  42004  mapdrvallem2  42091  mapd1o  42094  aks6d1c2  42569  elre0re  42693  prjspner1  43059  dffltz  43067  rexlimdv3d  43115  elrfi  43126  isnacs3  43142  eldiophb  43189  eldiophss  43206  diophren  43241  rencldnfilem  43248  pell1234qrdich  43289  pellfundex  43314  lsmfgcl  43502  kercvrlsm  43511  lmhmfgima  43512  lpirlnr  43545  hbtlem2  43552  hbtlem4  43554  hbtlem6  43557  rngunsnply  43597  onexoegt  43672  oaabsb  43722  cantnfresb  43752  omabs2  43760  tfsconcatrev  43776  restuni3  45548  limsupubuz  46141  stoweidlem57  46485  fourierdlem48  46582  fourierdlem49  46583  sge0le  46835  fsetsniunop  47497  cfsetsnfsetfo  47508  fcoresf1  47517  euoreqb  47557  modlt0b  47817  nndivides2  47832  imasetpreimafvbijlemf1  47864  imasetpreimafvbijlemfo  47865  iccpartrn  47890  iccpartiun  47894  iccpartnel  47898  paireqne  47971  reupr  47982  odz2prm2pw  48026  fmtnofac2lem  48031  prmdvdsfmtnof1lem2  48048  2pwp1prm  48052  mod42tp1mod8  48065  lighneallem3  48070  lighneallem4  48073  nprmdvdsfacm1  48087  ppivalnnprm  48088  ppivalnnnprmge6  48089  requad01  48097  requad2  48099  fppr2odd  48207  gbowpos  48235  gbowgt5  48238  gboge9  48240  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  isubgredg  48342  grimcnv  48364  uhgrimedgi  48366  isuspgrim0  48370  isuspgrimlem  48371  gricushgr  48393  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  grtrissvtx  48420  stgrusgra  48435  isubgr3stgrlem7  48448  gpgiedgdmellem  48522  gpgusgralem  48532  gpgvtxedg0  48539  gpgvtxedg1  48540  copisnmnd  48645  lidldomn1  48707  affinecomb1  49178  eenglngeehlnmlem2  49214  rrx2vlinest  49217  itsclquadb  49252  aacllem  50276