Theorem rexlimdva 3147

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-rex 3063

This theorem is referenced by:  rexlimdvaa  3148  rexlimivv  3191  rexlimdvv  3202  ssexnelpss  4105  ralxfrd2  5400  iunopeqop  5511  elsnxp  6280  foco2  7100  elunirn  7242  f1elima  7254  releldmdifi  8024  mpoexw  8058  xpord3pred  8132  sexp3  8133  tfrlem9a  8381  seqomlem2  8446  oawordexr  8551  odi  8574  oelimcl  8595  nnawordex  8632  nnaordex  8633  oaabs  8642  oaabs2  8643  omabs  8645  eldifsucnn  8658  coflton  8665  cofon1  8666  cofon2  8667  cofonr  8668  naddunif  8687  ectocld  8773  onfin  9225  dif1ennnALT  9272  isfinite2  9296  isfiniteg  9299  fofinf1o  9322  elfiun  9420  suplub2  9451  supisoex  9464  ordtypelem9  9516  ordtypelem10  9517  brwdom2  9563  brwdom3  9572  ttrcltr  9706  rankr1ai  9788  fodomfi2  10050  infpwfien  10052  dfac12r  10136  ackbij1  10228  cff1  10248  fin23lem21  10329  isf32lem2  10344  fin1a2lem11  10400  fin1a2lem13  10402  ficard  10555  gchina  10689  eltsk2g  10741  tskr1om2  10758  rankcf  10767  inatsk  10768  tskuni  10773  nqereu  10919  ltexnq  10965  1idpr  11019  suplem1pr  11042  supsrlem  11101  axpre-sup  11159  1re  11210  0re  11212  0cnALT  11444  negfi  12159  supaddc  12177  supadd  12178  supmul1  12179  supmul  12182  suprzcl2  12918  qmulz  12931  elpq  12955  qbtwnre  13174  ioo0  13345  ico0  13366  ioc0  13367  icc0  13368  addmodlteq  13907  fsequb  13936  hashdom  14335  ccats1alpha  14565  reuccatpfxs1lem  14692  shftlem  15011  rexuzre  15295  rexico  15296  caubnd  15301  limsupbnd1  15422  limsupbnd2  15423  rlim2lt  15437  rlim3  15438  lo1bdd2  15464  lo1bddrp  15465  o1lo1  15477  climuni  15492  climshftlem  15514  o1co  15526  rlimcn1  15528  climcn1  15532  o1rlimmul  15559  lo1le  15594  rlimno1  15596  isercoll  15610  caurcvg2  15620  serf0  15623  summolem2  15658  zsum  15660  fsum2dlem  15712  geomulcvg  15818  mertenslem2  15827  ntrivcvg  15839  zprod  15877  fprod2dlem  15920  dvds1lem  16207  dvdsexp2im  16266  odd2np1lem  16279  sqoddm1div8z  16293  ltoddhalfle  16300  halfleoddlt  16301  flodddiv4  16352  dvdssqim  16492  coprmdvds2  16587  divgcdcoprm0  16598  cncongr1  16600  cncongr2  16601  isprm5  16640  rpexp  16656  pythagtriplem1  16747  iserodd  16766  pc2dvds  16810  difsqpwdvds  16818  oddprmdvds  16834  prmpwdvds  16835  4sqlem11  16886  vdwapun  16905  vdwlem2  16913  vdwlem6  16917  vdwlem8  16919  vdwlem10  16921  vdwnnlem1  16926  vdwnnlem3  16928  0ram  16951  ramub1lem2  16958  ramcl  16960  cshwsiun  17031  cshwrepswhash1  17034  firest  17376  imasvscafn  17481  imasmnd2  18693  dfgrp3lem  18955  imasgrp2  18972  issubg4  19061  cycsubm  19117  gaorber  19213  orbsta  19218  pmtr3ncom  19384  psgnran  19424  odmulg  19465  odbezout  19467  gexdvdsi  19492  sylow1lem3  19509  odcau  19513  sylow2alem1  19526  sylow3lem6  19541  lsmelvalm  19560  efgrelexlemb  19659  efgredeu  19661  imasabl  19785  cyggeninv  19792  cygctb  19801  cyggexb  19808  dprdssv  19927  dprddisj2  19950  ablfacrplem  19976  pgpfac1lem2  19986  pgpfac1lem5  19990  ringinvnzdiv  20189  imasring  20218  dvdsrcl2  20257  dvdsrmul1  20260  lss1d  20799  lssats2  20836  lspsn  20838  lmhmima  20884  ring2idlqusb  21152  rngqiprngfulem2  21154  lpiss  21171  dvdsrzring  21315  pzriprnglem5  21339  pzriprnglem8  21342  pzriprnglem10  21344  pzriprnglem11  21345  znunit  21425  znrrg  21427  cygznlem3  21431  frgpcyg  21435  lindfrn  21683  mplcoe5lem  21903  mpfind  21979  gsummoncoe1  22148  mpfpf1  22191  pf1mpf  22192  mat1dimelbas  22294  scmatdmat  22338  scmataddcl  22339  scmatsubcl  22340  scmatmulcl  22341  cpmatacl  22539  chpscmat  22665  tgcl  22793  clsval2  22875  innei  22950  restcld  22997  restcldr  22999  ordtrest2lem  23028  cnprest  23114  lmss  23123  lmcls  23127  lmcnp  23129  isreg2  23202  cmpcovf  23216  cncmp  23217  cmpsub  23225  1stcrest  23278  2ndcrest  23279  1stccnp  23287  restnlly  23307  cldllycmp  23320  locfincmp  23351  txcnpi  23433  pthaus  23463  txtube  23465  txcmplem1  23466  txcmplem2  23467  txlm  23473  xkohaus  23478  xkococnlem  23484  xkococn  23485  kqfvima  23555  kqreglem1  23566  isfild  23683  filuni  23710  isufil2  23733  uffix  23746  rnelfm  23778  fmfnfmlem2  23780  fmfnfmlem4  23782  fmfnfm  23783  fmco  23786  fclsopn  23839  ufilcmp  23857  cnpfcf  23866  alexsublem  23869  alexsubALT  23876  cldsubg  23936  ghmcnp  23940  qustgpopn  23945  tsmsgsum  23964  tsmsres  23969  tsmsxplem1  23978  tsmsxp  23980  isucn2  24105  ucnprima  24108  imasdsf1olem  24200  blssps  24251  blss  24252  blssexps  24253  blssex  24254  mopni3  24324  blcld  24335  metrest  24354  metcnp3  24370  reperflem  24655  icccmplem3  24661  xrge0tsms  24671  mulc1cncf  24746  cncfco  24748  cnheibor  24802  bndth  24805  lebnumlem3  24810  xlebnum  24812  lebnumii  24813  nmhmcn  24968  cfil3i  25118  cmetcaulem  25137  cfilres  25145  bcthlem4  25176  ivthlem2  25302  ivthlem3  25303  ivthicc  25308  cniccbdd  25311  ovolunlem1  25347  ovoliunlem2  25353  ovolshftlem2  25360  ovolicc2  25372  iunmbl2  25407  dyadmax  25448  opnmbllem  25451  subopnmbl  25454  volivth  25457  ismbf3d  25504  mbfimaopn2  25507  mbfaddlem  25510  i1fmullem  25544  mbfi1fseqlem4  25569  bddiblnc  25692  ellimc3  25729  dvlip  25847  dvlip2  25849  c1liplem1  25850  dvgt0lem1  25856  dvivthlem2  25863  dvne0  25865  lhop1lem  25867  lhop2  25869  lhop  25870  tdeglem4  25916  tdeglem4OLD  25917  mdegnn0cl  25928  ply1divex  25993  dvdsq1p  26017  ig1peu  26028  elply2  26049  plypf1  26065  plydivex  26150  aalioulem3  26187  aalioulem5  26189  aaliou  26191  ulmshftlem  26241  ulmcau  26247  ulmss  26249  ulmbdd  26250  ulmcn  26251  radcnvlt1  26270  eflogeq  26451  efopn  26507  cxpeq  26607  angpieqvd  26678  xrlimcnp  26815  cxploglim  26825  ftalem2  26921  ftalem7  26926  isppw2  26962  dchrptlem1  27112  dchrptlem3  27114  dchrsum2  27116  lgsdchrval  27202  lgsdchr  27203  gausslemma2dlem1a  27213  lgsquadlem1  27228  2lgsoddprmlem2  27257  dchrisumlem3  27339  dchrisum0fno1  27359  pntlem3  27457  pntleml  27459  ostth3  27486  nosupno  27551  nosupbday  27553  noinfbday  27568  scutun12  27658  oldssmade  27719  addsproplem2  27802  addsuniflem  27833  negsid  27868  negsunif  27882  precsexlem6  28025  precsexlem7  28026  precsexlem11  28030  recut  28106  brcgr  28593  brbtwn2  28598  axbtwnid  28632  axcontlem7  28663  usgrnloopALT  28895  uhgrspansubgrlem  28982  nbuhgr  29035  nbupgr  29036  wwlksnextprop  29601  elwspths2on  29649  erclwwlktr  29710  clwwlknscsh  29750  erclwwlkntr  29759  hashecclwwlkn1  29765  umgrhashecclwwlk  29766  3cyclfrgrrn1  29973  frgrregorufr  30013  frgr2wwlk1  30017  ubthlem1  30558  ubthlem3  30560  htthlem  30605  omlsii  31091  spansncol  31256  nmopun  31702  nmcexi  31714  riesz1  31753  elpjrn  31878  cvcon3  31972  chcv1  32043  atcvatlem  32073  chirredi  32082  br8d  32274  xrge0tsmsd  32643  ordtrest2NEWlem  33357  lmxrge0  33387  esumfsup  33523  esumpcvgval  33531  measdivcstALTV  33678  eulerpartlemgh  33832  dstfrvunirn  33928  afsval  34138  erdszelem8  34644  erdszelem11  34647  erdsze2lem2  34650  connpconn  34681  sconnpi1  34685  cvmsss2  34720  cvmfolem  34725  cvmliftmolem2  34728  cvmliftlem15  34744  cvmlift2lem1  34748  cvmlift3lem4  34768  cvmlift3lem5  34769  satfdmlem  34814  fmla1  34833  gonarlem  34840  gonar  34841  goalrlem  34842  goalr  34843  fmla0disjsuc  34844  fmlasucdisj  34845  satffunlem1lem1  34848  satffunlem1lem2  34849  satffunlem2lem1  34850  mrsub0  34962  mrsubcn  34965  msubrn  34975  msubvrs  35006  br8  35187  br6  35188  br4  35189  cgrtriv  35435  btwntriv2  35445  btwncomim  35446  btwnswapid  35450  btwnintr  35452  btwnexch3  35453  btwnouttr2  35455  ifscgr  35477  cgrxfr  35488  btwnxfr  35489  btwnconn3  35536  segcon2  35538  brsegle  35541  seglecgr12im  35543  broutsideof3  35559  linethru  35586  elhf2  35608  opnregcld  35671  cldregopn  35672  neibastop2lem  35701  matunitlindflem1  36940  poimirlem16  36960  poimirlem17  36961  poimirlem19  36963  poimirlem20  36964  poimirlem24  36968  poimirlem29  36973  heicant  36979  opnmbllem0  36980  ismblfin  36985  itg2addnclem  36995  itg2addnclem3  36997  itg2gt0cn  36999  ftc1anclem5  37021  ftc2nc  37026  filbcmb  37064  fdc  37069  incsequz  37072  caushft  37085  istotbnd3  37095  equivbnd  37114  cntotbnd  37120  heibor1lem  37133  heibor1  37134  bfplem2  37147  divrngidl  37352  prnc  37391  lshpdisj  38313  cvrcon3b  38603  atnle  38643  hlhgt2  38716  hl0lt1N  38717  hl2at  38732  cvrexchlem  38746  cvratlem  38748  lvolnlelpln  38912  2lplnj  38947  ispsubcl2N  39274  lautcvr  39419  dva1dim  40312  dib1dim  40492  dib1dim2  40495  diclspsn  40521  dih1dimatlem  40656  dihlatat  40664  dihatexv  40665  dihatexv2  40666  lcfrlem9  40877  lcfrlem16  40885  mapdrvallem2  40972  mapd1o  40975  elre0re  41630  dvdsexpim  41674  prjspner1  41823  dffltz  41831  rexlimdv3d  41876  elrfi  41887  isnacs3  41903  eldiophb  41950  eldiophss  41967  diophren  42006  rencldnfilem  42013  pell1234qrdich  42054  pellfundex  42079  lsmfgcl  42271  kercvrlsm  42280  lmhmfgima  42281  lpirlnr  42314  hbtlem2  42321  hbtlem4  42323  hbtlem6  42326  rngunsnply  42370  onexoegt  42448  oaabsb  42499  cantnfresb  42529  omabs2  42537  tfsconcatrev  42553  restuni3  44261  limsupubuz  44880  stoweidlem57  45224  fourierdlem48  45321  fourierdlem49  45322  sge0le  45574  fsetsniunop  46210  cfsetsnfsetfo  46221  fcoresf1  46230  euoreqb  46268  imasetpreimafvbijlemf1  46523  imasetpreimafvbijlemfo  46524  iccpartrn  46549  iccpartiun  46553  iccpartnel  46557  paireqne  46630  reupr  46641  odz2prm2pw  46682  fmtnofac2lem  46687  prmdvdsfmtnof1lem2  46704  2pwp1prm  46708  mod42tp1mod8  46721  lighneallem3  46726  lighneallem4  46729  requad01  46740  requad2  46742  fppr2odd  46850  gbowpos  46878  gbowgt5  46881  gboge9  46883  nnsum4primesodd  46915  nnsum4primesoddALTV  46916  isomushgr  46945  isomuspgrlem2d  46950  copisnmnd  46998  lidldomn1  47060  affinecomb1  47542  eenglngeehlnmlem2  47578  rrx2vlinest  47581  itsclquadb  47616  rspceb2dv  47642  aacllem  48002