Theorem rexlimdva 3139

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

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

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 3063

This theorem is referenced by:  rexlimdvaa  3140  rexlimivv  3180  rexlimdvv  3194  rspceb2dv  3569  ssexnelpss  4057  ralxfrd2  5349  iunopeqop  5469  elsnxp  6249  foco2  7055  elunirn  7199  f1elima  7211  mptcnfimad  7932  releldmdifi  7991  mpoexw  8024  xpord3pred  8095  sexp3  8096  tfrlem9a  8318  seqomlem2  8383  oawordexr  8484  odi  8507  oelimcl  8529  nnawordex  8566  nnaordex  8567  oaabs  8577  oaabs2  8578  omabs  8580  eldifsucnn  8593  coflton  8600  cofon1  8601  cofon2  8602  cofonr  8603  naddunif  8622  ectocld  8722  onfin  9142  dif1ennnALT  9180  isfinite2  9201  isfiniteg  9203  fofinf1o  9235  elfiun  9336  suplub2  9367  supisoex  9381  ordtypelem9  9434  ordtypelem10  9435  brwdom2  9481  brwdom3  9490  ttrcltr  9628  rankr1ai  9713  fodomfi2  9973  infpwfien  9975  dfac12r  10060  ackbij1  10150  cff1  10171  fin23lem21  10252  isf32lem2  10267  fin1a2lem11  10323  fin1a2lem13  10325  ficard  10478  gchina  10613  eltsk2g  10665  tskr1om2  10682  rankcf  10691  inatsk  10692  tskuni  10697  nqereu  10843  ltexnq  10889  1idpr  10943  suplem1pr  10966  supsrlem  11025  axpre-sup  11083  1re  11135  0re  11137  0cnALT  11372  supaddc  12114  supadd  12115  supmul1  12116  supmul  12119  suprzcl2  12879  qmulz  12892  elpq  12916  qbtwnre  13142  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  addmodlteq  13899  fsequb  13928  hashdom  14332  ccats1alpha  14573  reuccatpfxs1lem  14699  shftlem  15021  rexuzre  15306  rexico  15307  caubnd  15312  limsupbnd1  15435  limsupbnd2  15436  rlim2lt  15450  rlim3  15451  lo1bdd2  15477  lo1bddrp  15478  o1lo1  15490  climuni  15505  climshftlem  15527  o1co  15539  rlimcn1  15541  climcn1  15545  o1rlimmul  15572  lo1le  15605  rlimno1  15607  isercoll  15621  caurcvg2  15631  serf0  15634  summolem2  15669  zsum  15671  fsum2dlem  15723  geomulcvg  15832  mertenslem2  15841  ntrivcvg  15853  zprod  15893  fprod2dlem  15936  dvds1lem  16227  dvdsexp2im  16287  odd2np1lem  16300  sqoddm1div8z  16314  ltoddhalfle  16321  halfleoddlt  16322  flodddiv4  16375  dvdssqim  16514  dvdsexpim  16515  coprmdvds2  16614  divgcdcoprm0  16625  cncongr1  16627  cncongr2  16628  isprm5  16668  rpexp  16683  pythagtriplem1  16778  iserodd  16797  pc2dvds  16841  difsqpwdvds  16849  oddprmdvds  16865  prmpwdvds  16866  4sqlem11  16917  vdwapun  16936  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  vdwlem10  16952  vdwnnlem1  16957  vdwnnlem3  16959  0ram  16982  ramub1lem2  16989  ramcl  16991  cshwsiun  17061  cshwrepswhash1  17064  firest  17386  imasvscafn  17492  imasmnd2  18733  dfgrp3lem  19005  imasgrp2  19022  issubg4  19112  cycsubm  19168  gaorber  19274  orbsta  19279  pmtr3ncom  19441  psgnran  19481  odmulg  19522  odbezout  19524  gexdvdsi  19549  sylow1lem3  19566  odcau  19570  sylow2alem1  19583  sylow3lem6  19598  lsmelvalm  19617  efgrelexlemb  19716  efgredeu  19718  imasabl  19842  cyggeninv  19849  cygctb  19858  cyggexb  19865  dprdssv  19984  dprddisj2  20007  ablfacrplem  20033  pgpfac1lem2  20043  pgpfac1lem5  20047  ringinvnzdiv  20273  imasring  20301  dvdsrcl2  20337  dvdsrmul1  20340  lss1d  20949  lssats2  20986  lspsn  20988  lmhmima  21034  ring2idlqusb  21300  rngqiprngfulem2  21302  lpiss  21319  dvdsrzring  21451  pzriprnglem5  21475  pzriprnglem8  21478  pzriprnglem10  21480  pzriprnglem11  21481  znunit  21553  znrrg  21555  cygznlem3  21559  frgpcyg  21563  lindfrn  21811  mplcoe5lem  22027  mpfind  22103  gsummoncoe1  22283  mpfpf1  22326  pf1mpf  22327  mat1dimelbas  22446  scmatdmat  22490  scmataddcl  22491  scmatsubcl  22492  scmatmulcl  22493  cpmatacl  22691  chpscmat  22817  tgcl  22944  clsval2  23025  innei  23100  restcld  23147  restcldr  23149  ordtrest2lem  23178  cnprest  23264  lmss  23273  lmcls  23277  lmcnp  23279  isreg2  23352  cmpcovf  23366  cncmp  23367  cmpsub  23375  1stcrest  23428  2ndcrest  23429  1stccnp  23437  restnlly  23457  cldllycmp  23470  locfincmp  23501  txcnpi  23583  pthaus  23613  txtube  23615  txcmplem1  23616  txcmplem2  23617  txlm  23623  xkohaus  23628  xkococnlem  23634  xkococn  23635  kqfvima  23705  kqreglem1  23716  isfild  23833  filuni  23860  isufil2  23883  uffix  23896  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  fmfnfm  23933  fmco  23936  fclsopn  23989  ufilcmp  24007  cnpfcf  24016  alexsublem  24019  alexsubALT  24026  cldsubg  24086  ghmcnp  24090  qustgpopn  24095  tsmsgsum  24114  tsmsres  24119  tsmsxplem1  24128  tsmsxp  24130  isucn2  24253  ucnprima  24256  imasdsf1olem  24348  blssps  24399  blss  24400  blssexps  24401  blssex  24402  mopni3  24469  blcld  24480  metrest  24499  metcnp3  24515  reperflem  24794  icccmplem3  24800  xrge0tsms  24810  mulc1cncf  24882  cncfco  24884  cnheibor  24932  bndth  24935  lebnumlem3  24940  xlebnum  24942  lebnumii  24943  nmhmcn  25097  cfil3i  25246  cmetcaulem  25265  cfilres  25273  bcthlem4  25304  ivthlem2  25429  ivthlem3  25430  ivthicc  25435  cniccbdd  25438  ovolunlem1  25474  ovoliunlem2  25480  ovolshftlem2  25487  ovolicc2  25499  iunmbl2  25534  dyadmax  25575  opnmbllem  25578  subopnmbl  25581  volivth  25584  ismbf3d  25631  mbfimaopn2  25634  mbfaddlem  25637  i1fmullem  25671  mbfi1fseqlem4  25695  bddiblnc  25819  ellimc3  25856  dvlip  25970  dvlip2  25972  c1liplem1  25973  dvgt0lem1  25979  dvivthlem2  25986  dvne0  25988  lhop1lem  25990  lhop2  25992  lhop  25993  tdeglem4  26035  mdegnn0cl  26046  ply1divex  26112  dvdsq1p  26138  ig1peu  26150  elply2  26171  plypf1  26187  plydivex  26274  aalioulem3  26311  aalioulem5  26313  aaliou  26315  ulmshftlem  26367  ulmcau  26373  ulmss  26375  ulmbdd  26376  ulmcn  26377  radcnvlt1  26396  eflogeq  26579  efopn  26635  cxpeq  26734  angpieqvd  26808  xrlimcnp  26945  cxploglim  26955  ftalem2  27051  ftalem7  27056  isppw2  27092  dchrptlem1  27241  dchrptlem3  27243  dchrsum2  27245  lgsdchrval  27331  lgsdchr  27332  gausslemma2dlem1a  27342  lgsquadlem1  27357  2lgsoddprmlem2  27386  dchrisumlem3  27468  dchrisum0fno1  27488  pntlem3  27586  pntleml  27588  ostth3  27615  nosupno  27681  nosupbday  27683  noinfbday  27698  cutsun12  27796  oldssmade  27873  addsproplem2  27976  addsuniflem  28007  addbdaylem  28023  negsid  28047  negsunif  28061  negleft  28064  negright  28065  precsexlem6  28218  precsexlem7  28219  precsexlem11  28223  bdayons  28282  onaddscl  28283  om2noseqlt  28305  noseqrdgfn  28312  n0fincut  28361  bdayn0sf1o  28376  dfnns2  28378  bdaypw2n0bndlem  28469  bdayfinbndlem1  28473  z12negscl  28484  z12zsodd  28488  z12bdaylem  28490  bdayfinlem  28492  recut  28500  elreno2  28501  brcgr  28983  brbtwn2  28988  axbtwnid  29022  axcontlem7  29053  usgrnloopALT  29286  uhgrspansubgrlem  29373  nbuhgr  29426  nbupgr  29427  wwlksnextprop  29995  elwspths2on  30045  elwspths2onw  30046  erclwwlktr  30107  clwwlknscsh  30147  erclwwlkntr  30156  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  3cyclfrgrrn1  30370  frgrregorufr  30410  frgr2wwlk1  30414  ubthlem1  30956  ubthlem3  30958  htthlem  31003  omlsii  31489  spansncol  31654  nmopun  32100  nmcexi  32112  riesz1  32151  elpjrn  32276  cvcon3  32370  chcv1  32441  atcvatlem  32471  chirredi  32480  br8d  32696  xrge0tsmsd  33149  ordtrest2NEWlem  34082  lmxrge0  34112  esumfsup  34230  esumpcvgval  34238  measdivcstALTV  34385  eulerpartlemgh  34538  dstfrvunirn  34635  afsval  34831  onvf1odlem4  35304  erdszelem8  35396  erdszelem11  35399  erdsze2lem2  35402  connpconn  35433  sconnpi1  35437  cvmsss2  35472  cvmfolem  35477  cvmliftmolem2  35480  cvmliftlem15  35496  cvmlift2lem1  35500  cvmlift3lem4  35520  cvmlift3lem5  35521  satfdmlem  35566  fmla1  35585  gonarlem  35592  gonar  35593  goalrlem  35594  goalr  35595  fmla0disjsuc  35596  fmlasucdisj  35597  satffunlem1lem1  35600  satffunlem1lem2  35601  satffunlem2lem1  35602  mrsub0  35714  mrsubcn  35717  msubrn  35727  msubvrs  35758  br8  35954  br6  35955  br4  35956  cgrtriv  36200  btwntriv2  36210  btwncomim  36211  btwnswapid  36215  btwnintr  36217  btwnexch3  36218  btwnouttr2  36220  ifscgr  36242  cgrxfr  36253  btwnxfr  36254  btwnconn3  36301  segcon2  36303  brsegle  36306  seglecgr12im  36308  broutsideof3  36324  linethru  36351  elhf2  36373  opnregcld  36528  cldregopn  36529  neibastop2lem  36558  tr0elw  36682  tr0el  36683  matunitlindflem1  37951  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem24  37979  poimirlem29  37984  heicant  37990  opnmbllem0  37991  ismblfin  37996  itg2addnclem  38006  itg2addnclem3  38008  itg2gt0cn  38010  ftc1anclem5  38032  ftc2nc  38037  filbcmb  38075  fdc  38080  incsequz  38083  caushft  38096  istotbnd3  38106  equivbnd  38125  cntotbnd  38131  heibor1lem  38144  heibor1  38145  bfplem2  38158  divrngidl  38363  prnc  38402  lshpdisj  39447  cvrcon3b  39737  atnle  39777  hlhgt2  39849  hl0lt1N  39850  hl2at  39865  cvrexchlem  39879  cvratlem  39881  lvolnlelpln  40045  2lplnj  40080  ispsubcl2N  40407  lautcvr  40552  dva1dim  41445  dib1dim  41625  dib1dim2  41628  diclspsn  41654  dih1dimatlem  41789  dihlatat  41797  dihatexv  41798  dihatexv2  41799  lcfrlem9  42010  lcfrlem16  42018  mapdrvallem2  42105  mapd1o  42108  aks6d1c2  42583  elre0re  42707  prjspner1  43073  dffltz  43081  rexlimdv3d  43129  elrfi  43140  isnacs3  43156  eldiophb  43203  eldiophss  43220  diophren  43259  rencldnfilem  43266  pell1234qrdich  43307  pellfundex  43332  lsmfgcl  43520  kercvrlsm  43529  lmhmfgima  43530  lpirlnr  43563  hbtlem2  43570  hbtlem4  43572  hbtlem6  43575  rngunsnply  43615  onexoegt  43690  oaabsb  43740  cantnfresb  43770  omabs2  43778  tfsconcatrev  43794  restuni3  45566  limsupubuz  46159  stoweidlem57  46503  fourierdlem48  46600  fourierdlem49  46601  sge0le  46853  fsetsniunop  47509  cfsetsnfsetfo  47520  fcoresf1  47529  euoreqb  47569  modlt0b  47829  nndivides2  47844  imasetpreimafvbijlemf1  47876  imasetpreimafvbijlemfo  47877  iccpartrn  47902  iccpartiun  47906  iccpartnel  47910  paireqne  47983  reupr  47994  odz2prm2pw  48038  fmtnofac2lem  48043  prmdvdsfmtnof1lem2  48060  2pwp1prm  48064  mod42tp1mod8  48077  lighneallem3  48082  lighneallem4  48085  nprmdvdsfacm1  48099  ppivalnnprm  48100  ppivalnnnprmge6  48101  requad01  48109  requad2  48111  fppr2odd  48219  gbowpos  48247  gbowgt5  48250  gboge9  48252  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  isubgredg  48354  grimcnv  48376  uhgrimedgi  48378  isuspgrim0  48382  isuspgrimlem  48383  gricushgr  48405  clnbgrgrimlem  48421  clnbgrgrim  48422  grimedg  48423  grtrissvtx  48432  stgrusgra  48447  isubgr3stgrlem7  48460  gpgiedgdmellem  48534  gpgusgralem  48544  gpgvtxedg0  48551  gpgvtxedg1  48552  copisnmnd  48657  lidldomn1  48719  affinecomb1  49190  eenglngeehlnmlem2  49226  rrx2vlinest  49229  itsclquadb  49264  aacllem  50288