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  6294  foco2  7109  elunirn  7255  f1elima  7267  mptcnfimad  7998  releldmdifi  8056  mpoexw  8091  xpord3pred  8169  sexp3  8170  tfrlem9a  8394  seqomlem2  8461  oawordexr  8564  odi  8587  oelimcl  8609  nnawordex  8646  nnaordex  8647  oaabs  8657  oaabs2  8658  omabs  8660  eldifsucnn  8673  coflton  8680  cofon1  8681  cofon2  8682  cofonr  8683  naddunif  8703  ectocld  8803  onfin  9230  dif1ennnALT  9268  isfinite2  9290  isfiniteg  9292  fofinf1o  9321  elfiun  9422  suplub2  9453  supisoex  9467  ordtypelem9  9520  ordtypelem10  9521  brwdom2  9567  brwdom3  9576  ttrcltr  9717  rankr1ai  9806  elhf2  9910  fodomfi2  10139  infpwfien  10141  dfac12r  10225  ackbij1  10315  cff1  10336  fin23lem21  10417  isf32lem2  10432  fin1a2lem11  10488  fin1a2lem13  10490  ficard  10649  gchina  10784  eltsk2g  10836  tskhf  10853  rankcf  10862  inatsk  10863  tskuni  10868  nqereu  11014  ltexnq  11060  1idpr  11114  suplem1pr  11137  supsrlem  11196  axpre-sup  11254  1re  11308  0re  11310  0cnALT  11545  supaddc  12284  supadd  12285  supmul1  12286  supmul  12289  suprzcl2  13065  qmulz  13078  elpq  13103  qbtwnre  13329  ioo0  13501  ico0  13522  ioc0  13523  icc0  13524  addmodlteq  14089  fsequb  14118  hashdom  14523  ccats1alpha  14767  reuccatpfxs1lem  14895  shftlem  15221  rexuzre  15520  rexico  15521  caubnd  15526  limsupbnd1  15649  limsupbnd2  15650  rlim2lt  15664  rlim3  15665  lo1bdd2  15691  lo1bddrp  15692  o1lo1  15704  climuni  15719  climshftlem  15741  o1co  15753  rlimcn1  15755  climcn1  15759  o1rlimmul  15786  lo1le  15819  rlimno1  15821  isercoll  15835  caurcvg2  15845  serf0  15848  summolem2  15882  zsum  15884  fsum2dlem  15936  geomulcvg  16045  mertenslem2  16054  ntrivcvg  16066  zprod  16104  fprod2dlem  16147  dvds1lem  16437  dvdsexp2im  16497  odd2np1lem  16510  sqoddm1div8z  16524  ltoddhalfle  16531  halfleoddlt  16532  flodddiv4  16585  dvdssqim  16727  dvdsexpim  16728  coprmdvds2  16829  divgcdcoprm0  16840  cncongr1  16842  cncongr2  16843  isprm5  16883  rpexp  16898  pythagtriplem1  16994  iserodd  17013  pc2dvds  17057  difsqpwdvds  17065  oddprmdvds  17081  prmpwdvds  17082  4sqlem11  17133  vdwapun  17152  vdwlem2  17160  vdwlem6  17164  vdwlem8  17166  vdwlem10  17168  vdwnnlem1  17173  vdwnnlem3  17175  0ram  17198  ramub1lem2  17205  ramcl  17207  cshwsiun  17277  cshwrepswhash1  17280  firest  17603  imasvscafn  17709  imasmgm2  18863  imasmnd2  18968  dfgrp3lem  19248  imasgrp2  19265  issubg4  19356  cycsubm  19417  gaorber  19522  orbsta  19527  pmtr3ncom  19689  psgnran  19729  odmulg  19770  odbezout  19772  gexdvdsi  19797  sylow1lem3  19814  odcau  19818  sylow2alem1  19831  sylow3lem6  19846  lsmelvalm  19865  efgrelexlemb  19964  efgredeu  19966  imasabl  20090  cyggeninv  20097  cygctb  20106  cyggexb  20113  dprdssv  20232  dprddisj2  20255  ablfacrplem  20281  pgpfac1lem2  20291  pgpfac1lem5  20295  ringinvnzdiv  20532  imasring  20560  dvdsrcl2  20596  dvdsrmul1  20599  lss1d  21238  lssats2  21275  lspsn  21277  lmhmima  21322  rspsn0  21526  ring2idlqusb  21606  rngqiprngfulem2  21608  lpiss  21653  dvdsrzring  21767  pzriprnglem5  21791  pzriprnglem8  21794  pzriprnglem10  21796  pzriprnglem11  21797  znunit  21869  znrrg  21871  cygznlem3  21875  frgpcyg  21879  lindfrn  22127  mplcoe5lem  22348  mpfind  22424  gsummoncoe1  22626  mpfpf1  22669  pf1mpf  22670  mat1dimelbas  22786  scmatdmat  22830  scmataddcl  22831  scmatsubcl  22832  scmatmulcl  22833  matunitlindflem1  22994  cpmatacl  23034  chpscmat  23160  tgcl  23287  clsval2  23368  innei  23443  restcld  23490  restcldr  23492  ordtrest2lem  23521  cnprest  23607  lmss  23616  lmcls  23620  lmcnp  23622  isreg2  23695  cmpcovf  23709  cncmp  23710  cmpsub  23718  1stcrest  23771  2ndcrest  23772  1stccnp  23781  restnlly  23801  cldllycmp  23814  locfincmp  23845  txcnpi  23927  pthaus  23957  txtube  23959  txcmplem1  23960  txcmplem2  23961  txlm  23967  xkohaus  23972  xkococnlem  23978  xkococn  23979  kqfvima  24049  kqreglem1  24060  isfild  24177  filuni  24204  isufil2  24227  uffix  24240  rnelfm  24272  fmfnfmlem2  24274  fmfnfmlem4  24276  fmfnfm  24277  fmco  24280  fclsopn  24333  ufilcmp  24351  cnpfcf  24360  alexsublem  24363  alexsubALT  24370  cldsubg  24430  ghmcnp  24434  qustgpopn  24439  tsmsgsum  24458  tsmsres  24463  tsmsxplem1  24472  tsmsxp  24474  isucn2  24597  ucnprima  24600  imasdsf1olem  24692  blssps  24743  blss  24744  blssexps  24745  blssex  24746  mopni3  24813  blcld  24824  metrest  24843  metcnp3  24859  reperflem  25138  icccmplem3  25144  xrge0tsms  25154  mulc1cncf  25226  cncfco  25228  cnheibor  25276  bndth  25279  lebnumlem3  25284  xlebnum  25286  lebnumii  25287  nmhmcn  25441  cfil3i  25590  cmetcaulem  25609  cfilres  25617  bcthlem4  25648  ivthlem2  25773  ivthlem3  25774  ivthicc  25779  cniccbdd  25782  ovolunlem1  25818  ovoliunlem2  25824  ovolshftlem2  25831  ovolicc2  25843  iunmbl2  25878  dyadmax  25919  opnmbllem  25922  subopnmbl  25925  volivth  25928  ismbf3d  25975  mbfimaopn2  25978  mbfaddlem  25981  i1fmullem  26015  mbfi1fseqlem4  26039  bddiblnc  26162  ellimc3  26199  dvlip  26313  dvlip2  26315  c1liplem1  26316  dvgt0lem1  26322  dvivthlem2  26329  dvne0  26331  lhop1lem  26333  lhop2  26335  lhop  26336  tdeglem4  26378  mdegnn0cl  26389  ply1divex  26455  dvdsq1p  26481  ig1peu  26493  elply2  26514  plypf1  26531  plydivex  26618  aalioulem3  26661  aalioulem5  26663  aaliou  26665  ulmshftlem  26716  ulmcau  26722  ulmss  26724  ulmbdd  26725  ulmcn  26726  radcnvlt1  26745  eflogeq  26930  efopn  26986  cxpeq  27085  angpieqvd  27159  xrlimcnp  27296  cxploglim  27305  ftalem2  27401  ftalem7  27406  isppw2  27442  dchrptlem1  27591  dchrptlem3  27593  dchrsum2  27595  lgsdchrval  27681  lgsdchr  27682  gausslemma2dlem1a  27692  lgsquadlem1  27707  2lgsoddprmlem2  27736  dchrisumlem3  27818  dchrisum0fno1  27838  pntlem3  27936  pntleml  27938  ostth3  27965  fltoprm  27995  nosupno  28060  nosupbday  28062  noinfbday  28077  cutsun12  28176  oldssmade  28253  addsproplem2  28356  addsuniflem  28387  addbdaylem  28403  negsid  28427  negsunif  28441  negleft  28444  negright  28445  precsexlem6  28598  precsexlem7  28599  precsexlem11  28603  bdayons  28662  onaddscl  28663  om2noseqlt  28685  noseqrdgfn  28692  n0fincut  28741  bdayn0sf1o  28756  dfnns2  28758  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  z12negscl  28864  z12zsodd  28868  z12bdaylem  28870  bdayfinlem  28872  recut  28880  elreno2  28881  brcgr  29478  brbtwn2  29483  axbtwnid  29517  axcontlem7  29548  usgrnloopALT  29784  uhgrspansubgrlem  29871  nbuhgr  29924  nbupgr  29925  wwlksnextprop  30501  elwspths2on  30551  elwspths2onw  30552  erclwwlktr  30613  clwwlknscsh  30653  erclwwlkntr  30662  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  3cyclfrgrrn1  30886  frgrregorufr  30926  frgr2wwlk1  30930  ubthlem1  31472  ubthlem3  31474  htthlem  31519  omlsii  32005  spansncol  32170  nmopun  32616  nmcexi  32628  riesz1  32667  elpjrn  32792  cvcon3  32886  chcv1  32957  atcvatlem  32987  chirredi  32996  br8d  33202  xrge0tsmsd  33634  ordtrest2NEWlem  34554  lmxrge0  34584  esumfsup  34702  esumpcvgval  34710  measdivcstALTV  34858  eulerpartlemgh  35010  dstfrvunirn  35107  afsval  35303  onvf1odlem4  35885  onprcf1acwevdlem1  35895  erdszelem8  35963  erdszelem11  35966  erdsze2lem2  35969  connpconn  36000  sconnpi1  36004  cvmsss2  36039  cvmfolem  36044  cvmliftmolem2  36047  cvmliftlem15  36063  cvmlift2lem1  36067  cvmlift3lem4  36087  cvmlift3lem5  36088  satfdmlem  36133  fmla1  36152  gonarlem  36159  gonar  36160  goalrlem  36161  goalr  36162  fmla0disjsuc  36163  fmlasucdisj  36164  satffunlem1lem1  36167  satffunlem1lem2  36168  satffunlem2lem1  36169  mrsub0  36281  mrsubcn  36284  msubrn  36294  msubvrs  36325  br8  36521  br6  36522  br4  36523  cgrtriv  36767  btwntriv2  36777  btwncomim  36778  btwnswapid  36782  btwnintr  36784  btwnexch3  36785  btwnouttr2  36787  ifscgr  36809  cgrxfr  36820  btwnxfr  36821  btwnconn3  36868  segcon2  36870  brsegle  36873  seglecgr12im  36875  broutsideof3  36891  linethru  36918  nmulprop  36939  opnregcld  37118  cldregopn  37119  neibastop2lem  37148  tr0elw  37272  tr0el  37273  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem24  38562  poimirlem29  38567  heicant  38573  opnmbllem0  38574  ismblfin  38579  itg2addnclem  38589  itg2addnclem3  38591  itg2gt0cn  38593  ftc1anclem5  38615  ftc2nc  38620  filbcmb  38674  fdc  38679  incsequz  38682  caushft  38695  istotbnd3  38705  equivbnd  38724  cntotbnd  38730  heibor1lem  38743  heibor1  38744  bfplem2  38757  divrngidl  38962  prnc  39001  lshpdisj  40044  cvrcon3b  40334  atnle  40374  hlhgt2  40446  hl0lt1N  40447  hl2at  40462  cvrexchlem  40476  cvratlem  40478  lvolnlelpln  40642  2lplnj  40677  ispsubcl2N  41004  lautcvr  41149  dva1dim  42042  dib1dim  42222  dib1dim2  42225  diclspsn  42251  dih1dimatlem  42386  dihlatat  42394  dihatexv  42395  dihatexv2  42396  lcfrlem9  42607  lcfrlem16  42615  mapdrvallem2  42702  mapd1o  42705  aks6d1c2  43180  elre0re  43305  dffltz  43670  rexlimdv3d  43693  elrfi  43704  isnacs3  43720  eldiophb  43767  eldiophss  43784  diophren  43819  rencldnfilem  43826  pell1234qrdich  43867  pellfundex  43892  lsmfgcl  44075  kercvrlsm  44084  lmhmfgima  44085  lpirlnr  44118  hbtlem2  44125  hbtlem4  44127  hbtlem6  44130  rngunsnply  44170  onexoegt  44245  oaabsb  44295  cantnfresb  44325  omabs2  44333  tfsconcatrev  44349  restuni3  46132  limsupubuz  46722  stoweidlem57  47066  fourierdlem48  47163  fourierdlem49  47164  sge0le  47416  fsetsniunop  48118  cfsetsnfsetfo  48129  fcoresf1  48138  euoreqb  48178  modlt0b  48438  nndivides2  48453  imasetpreimafvbijlemf1  48485  imasetpreimafvbijlemfo  48486  iccpartrn  48511  iccpartiun  48515  iccpartnel  48519  paireqne  48592  reupr  48603  odz2prm2pw  48647  fmtnofac2lem  48652  prmdvdsfmtnof1lem2  48669  2pwp1prm  48673  mod42tp1mod8  48686  lighneallem3  48691  lighneallem4  48694  nprmdvdsfacm1  48708  ppivalnnprm  48709  ppivalnnnprmge6  48710  requad01  48718  requad2  48720  fppr2odd  48828  gbowpos  48856  gbowgt5  48859  gboge9  48861  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  isubgredg  48963  grimcnv  48985  uhgrimedgi  48987  isuspgrim0  48991  isuspgrimlem  48992  gricushgr  49014  clnbgrgrimlem  49030  clnbgrgrim  49031  grimedg  49032  grtrissvtx  49041  stgrusgra  49056  isubgr3stgrlem7  49069  gpgiedgdmellem  49143  gpgusgralem  49153  gpgvtxedg0  49160  gpgvtxedg1  49161  copisnmnd  49265  lidldomn1  49327  affinecomb1  49813  eenglngeehlnmlem2  49849  rrx2vlinest  49852  itsclquadb  49887  aacllem  50938