Theorem rexlimdva 3166

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimdvaa  3167  rexlimivv  3207  rexlimdvv  3221  rspceb2dv  3586  ssexnelpss  4072  ralxfrd2  5385  iunopeqop  5506  iunopeqopOLD  5507  elsnxp  6294  foco2  7106  elunirn  7251  f1elima  7263  mptcnfimad  7984  releldmdifi  8043  mpoexw  8076  xpord3pred  8149  sexp3  8150  tfrlem9a  8374  seqomlem2  8439  oawordexr  8542  odi  8565  oelimcl  8587  nnawordex  8624  nnaordex  8625  oaabs  8635  oaabs2  8636  omabs  8638  eldifsucnn  8651  coflton  8658  cofon1  8659  cofon2  8660  cofonr  8661  naddunif  8681  ectocld  8781  onfin  9200  dif1ennnALT  9238  isfinite2  9259  isfiniteg  9261  fofinf1o  9290  elfiun  9391  suplub2  9422  supisoex  9436  ordtypelem9  9489  ordtypelem10  9490  brwdom2  9536  brwdom3  9545  ttrcltr  9686  rankr1ai  9771  fodomfi2  10045  infpwfien  10047  dfac12r  10131  ackbij1  10221  cff1  10243  fin23lem21  10324  isf32lem2  10339  fin1a2lem11  10395  fin1a2lem13  10397  ficard  10550  gchina  10685  eltsk2g  10737  tskr1om2  10754  rankcf  10763  inatsk  10764  tskuni  10769  nqereu  10915  ltexnq  10961  1idpr  11015  suplem1pr  11038  supsrlem  11097  axpre-sup  11155  1re  11209  0re  11211  0cnALT  11446  supaddc  12183  supadd  12184  supmul1  12185  supmul  12188  suprzcl2  12963  qmulz  12976  elpq  13000  qbtwnre  13226  ioo0  13398  ico0  13419  ioc0  13420  icc0  13421  addmodlteq  13984  fsequb  14013  hashdom  14417  ccats1alpha  14659  reuccatpfxs1lem  14785  shftlem  15107  rexuzre  15406  rexico  15407  caubnd  15412  limsupbnd1  15535  limsupbnd2  15536  rlim2lt  15550  rlim3  15551  lo1bdd2  15577  lo1bddrp  15578  o1lo1  15590  climuni  15605  climshftlem  15627  o1co  15639  rlimcn1  15641  climcn1  15645  o1rlimmul  15672  lo1le  15705  rlimno1  15707  isercoll  15721  caurcvg2  15731  serf0  15734  summolem2  15769  zsum  15771  fsum2dlem  15823  geomulcvg  15932  mertenslem2  15941  ntrivcvg  15953  zprod  15993  fprod2dlem  16036  dvds1lem  16326  dvdsexp2im  16386  odd2np1lem  16399  sqoddm1div8z  16413  ltoddhalfle  16420  halfleoddlt  16421  flodddiv4  16474  dvdssqim  16613  dvdsexpim  16614  coprmdvds2  16713  divgcdcoprm0  16724  cncongr1  16726  cncongr2  16727  isprm5  16767  rpexp  16782  pythagtriplem1  16877  iserodd  16896  pc2dvds  16940  difsqpwdvds  16948  oddprmdvds  16964  prmpwdvds  16965  4sqlem11  17016  vdwapun  17035  vdwlem2  17043  vdwlem6  17047  vdwlem8  17049  vdwlem10  17051  vdwnnlem1  17056  vdwnnlem3  17058  0ram  17081  ramub1lem2  17088  ramcl  17090  cshwsiun  17160  cshwrepswhash1  17163  firest  17486  imasvscafn  17592  imasmnd2  18833  dfgrp3lem  19105  imasgrp2  19122  issubg4  19213  cycsubm  19274  gaorber  19379  orbsta  19384  pmtr3ncom  19546  psgnran  19586  odmulg  19627  odbezout  19629  gexdvdsi  19654  sylow1lem3  19671  odcau  19675  sylow2alem1  19688  sylow3lem6  19703  lsmelvalm  19722  efgrelexlemb  19821  efgredeu  19823  imasabl  19947  cyggeninv  19954  cygctb  19963  cyggexb  19970  dprdssv  20089  dprddisj2  20112  ablfacrplem  20138  pgpfac1lem2  20148  pgpfac1lem5  20152  ringinvnzdiv  20385  imasring  20413  dvdsrcl2  20449  dvdsrmul1  20452  lss1d  21065  lssats2  21102  lspsn  21104  lmhmima  21149  rspsn0  21353  ring2idlqusb  21431  rngqiprngfulem2  21433  lpiss  21478  dvdsrzring  21592  pzriprnglem5  21616  pzriprnglem8  21619  pzriprnglem10  21621  pzriprnglem11  21622  znunit  21694  znrrg  21696  cygznlem3  21700  frgpcyg  21704  lindfrn  21952  mplcoe5lem  22171  mpfind  22247  gsummoncoe1  22449  mpfpf1  22492  pf1mpf  22493  mat1dimelbas  22609  scmatdmat  22653  scmataddcl  22654  scmatsubcl  22655  scmatmulcl  22656  cpmatacl  22854  chpscmat  22980  tgcl  23107  clsval2  23188  innei  23263  restcld  23310  restcldr  23312  ordtrest2lem  23341  cnprest  23427  lmss  23436  lmcls  23440  lmcnp  23442  isreg2  23515  cmpcovf  23529  cncmp  23530  cmpsub  23538  1stcrest  23591  2ndcrest  23592  1stccnp  23600  restnlly  23620  cldllycmp  23633  locfincmp  23664  txcnpi  23746  pthaus  23776  txtube  23778  txcmplem1  23779  txcmplem2  23780  txlm  23786  xkohaus  23791  xkococnlem  23797  xkococn  23798  kqfvima  23868  kqreglem1  23879  isfild  23996  filuni  24023  isufil2  24046  uffix  24059  rnelfm  24091  fmfnfmlem2  24093  fmfnfmlem4  24095  fmfnfm  24096  fmco  24099  fclsopn  24152  ufilcmp  24170  cnpfcf  24179  alexsublem  24182  alexsubALT  24189  cldsubg  24249  ghmcnp  24253  qustgpopn  24258  tsmsgsum  24277  tsmsres  24282  tsmsxplem1  24291  tsmsxp  24293  isucn2  24416  ucnprima  24419  imasdsf1olem  24511  blssps  24562  blss  24563  blssexps  24564  blssex  24565  mopni3  24632  blcld  24643  metrest  24662  metcnp3  24678  reperflem  24957  icccmplem3  24963  xrge0tsms  24973  mulc1cncf  25045  cncfco  25047  cnheibor  25095  bndth  25098  lebnumlem3  25103  xlebnum  25105  lebnumii  25106  nmhmcn  25260  cfil3i  25409  cmetcaulem  25428  cfilres  25436  bcthlem4  25467  ivthlem2  25592  ivthlem3  25593  ivthicc  25598  cniccbdd  25601  ovolunlem1  25637  ovoliunlem2  25643  ovolshftlem2  25650  ovolicc2  25662  iunmbl2  25697  dyadmax  25738  opnmbllem  25741  subopnmbl  25744  volivth  25747  ismbf3d  25794  mbfimaopn2  25797  mbfaddlem  25800  i1fmullem  25834  mbfi1fseqlem4  25858  bddiblnc  25982  ellimc3  26019  dvlip  26133  dvlip2  26135  c1liplem1  26136  dvgt0lem1  26142  dvivthlem2  26149  dvne0  26151  lhop1lem  26153  lhop2  26155  lhop  26156  tdeglem4  26198  mdegnn0cl  26209  ply1divex  26275  dvdsq1p  26301  ig1peu  26313  elply2  26334  plypf1  26350  plydivex  26439  aalioulem3  26478  aalioulem5  26480  aaliou  26482  ulmshftlem  26533  ulmcau  26539  ulmss  26541  ulmbdd  26542  ulmcn  26543  radcnvlt1  26562  eflogeq  26748  efopn  26804  cxpeq  26903  angpieqvd  26977  xrlimcnp  27114  cxploglim  27123  ftalem2  27219  ftalem7  27224  isppw2  27260  dchrptlem1  27409  dchrptlem3  27411  dchrsum2  27413  lgsdchrval  27499  lgsdchr  27500  gausslemma2dlem1a  27510  lgsquadlem1  27525  2lgsoddprmlem2  27554  dchrisumlem3  27636  dchrisum0fno1  27656  pntlem3  27754  pntleml  27756  ostth3  27783  nosupno  27848  nosupbday  27850  noinfbday  27865  cutsun12  27964  oldssmade  28041  addsproplem2  28144  addsuniflem  28175  addbdaylem  28191  negsid  28215  negsunif  28229  negleft  28232  negright  28233  precsexlem6  28386  precsexlem7  28387  precsexlem11  28391  bdayons  28450  onaddscl  28451  om2noseqlt  28473  noseqrdgfn  28480  n0fincut  28529  bdayn0sf1o  28544  dfnns2  28546  bdaypw2n0bndlem  28637  bdayfinbndlem1  28641  z12negscl  28652  z12zsodd  28656  z12bdaylem  28658  bdayfinlem  28660  recut  28668  elreno2  28669  brcgr  29231  brbtwn2  29236  axbtwnid  29270  axcontlem7  29301  usgrnloopALT  29534  uhgrspansubgrlem  29621  nbuhgr  29674  nbupgr  29675  wwlksnextprop  30242  elwspths2on  30292  elwspths2onw  30293  erclwwlktr  30354  clwwlknscsh  30394  erclwwlkntr  30403  hashecclwwlkn1  30409  umgrhashecclwwlk  30410  3cyclfrgrrn1  30617  frgrregorufr  30657  frgr2wwlk1  30661  ubthlem1  31203  ubthlem3  31205  htthlem  31250  omlsii  31736  spansncol  31901  nmopun  32347  nmcexi  32359  riesz1  32398  elpjrn  32523  cvcon3  32617  chcv1  32688  atcvatlem  32718  chirredi  32727  br8d  32934  xrge0tsmsd  33374  ordtrest2NEWlem  34293  lmxrge0  34323  esumfsup  34441  esumpcvgval  34449  measdivcstALTV  34596  eulerpartlemgh  34749  dstfrvunirn  34846  afsval  35042  onvf1odlem4  35571  erdszelem8  35671  erdszelem11  35674  erdsze2lem2  35677  connpconn  35708  sconnpi1  35712  cvmsss2  35747  cvmfolem  35752  cvmliftmolem2  35755  cvmliftlem15  35771  cvmlift2lem1  35775  cvmlift3lem4  35795  cvmlift3lem5  35796  satfdmlem  35841  fmla1  35860  gonarlem  35867  gonar  35868  goalrlem  35869  goalr  35870  fmla0disjsuc  35871  fmlasucdisj  35872  satffunlem1lem1  35875  satffunlem1lem2  35876  satffunlem2lem1  35877  mrsub0  35989  mrsubcn  35992  msubrn  36002  msubvrs  36033  br8  36229  br6  36230  br4  36231  cgrtriv  36475  btwntriv2  36485  btwncomim  36486  btwnswapid  36490  btwnintr  36492  btwnexch3  36493  btwnouttr2  36495  ifscgr  36517  cgrxfr  36528  btwnxfr  36529  btwnconn3  36576  segcon2  36578  brsegle  36581  seglecgr12im  36583  broutsideof3  36599  linethru  36626  elhf2  36648  nmulprop  36663  opnregcld  36822  cldregopn  36823  neibastop2lem  36852  tr0elw  36976  tr0el  36977  matunitlindflem1  38248  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem24  38276  poimirlem29  38281  heicant  38287  opnmbllem0  38288  ismblfin  38293  itg2addnclem  38303  itg2addnclem3  38305  itg2gt0cn  38307  ftc1anclem5  38329  ftc2nc  38334  filbcmb  38372  fdc  38377  incsequz  38380  caushft  38393  istotbnd3  38403  equivbnd  38422  cntotbnd  38428  heibor1lem  38441  heibor1  38442  bfplem2  38455  divrngidl  38660  prnc  38699  lshpdisj  39742  cvrcon3b  40032  atnle  40072  hlhgt2  40144  hl0lt1N  40145  hl2at  40160  cvrexchlem  40174  cvratlem  40176  lvolnlelpln  40340  2lplnj  40375  ispsubcl2N  40702  lautcvr  40847  dva1dim  41740  dib1dim  41920  dib1dim2  41923  diclspsn  41949  dih1dimatlem  42084  dihlatat  42092  dihatexv  42093  dihatexv2  42094  lcfrlem9  42305  lcfrlem16  42313  mapdrvallem2  42400  mapd1o  42403  aks6d1c2  42878  elre0re  43003  prjspner1  43341  dffltz  43349  rexlimdv3d  43397  elrfi  43408  isnacs3  43424  eldiophb  43471  eldiophss  43488  diophren  43523  rencldnfilem  43530  pell1234qrdich  43571  pellfundex  43596  lsmfgcl  43784  kercvrlsm  43793  lmhmfgima  43794  lpirlnr  43827  hbtlem2  43834  hbtlem4  43836  hbtlem6  43839  rngunsnply  43879  onexoegt  43954  oaabsb  44004  cantnfresb  44034  omabs2  44042  tfsconcatrev  44058  restuni3  45819  limsupubuz  46410  stoweidlem57  46754  fourierdlem48  46851  fourierdlem49  46852  sge0le  47104  fsetsniunop  47769  cfsetsnfsetfo  47780  fcoresf1  47789  euoreqb  47829  modlt0b  48089  nndivides2  48104  imasetpreimafvbijlemf1  48136  imasetpreimafvbijlemfo  48137  iccpartrn  48162  iccpartiun  48166  iccpartnel  48170  paireqne  48243  reupr  48254  odz2prm2pw  48298  fmtnofac2lem  48303  prmdvdsfmtnof1lem2  48320  2pwp1prm  48324  mod42tp1mod8  48337  lighneallem3  48342  lighneallem4  48345  nprmdvdsfacm1  48359  ppivalnnprm  48360  ppivalnnnprmge6  48361  requad01  48369  requad2  48371  fppr2odd  48479  gbowpos  48507  gbowgt5  48510  gboge9  48512  nnsum4primesodd  48544  nnsum4primesoddALTV  48545  isubgredg  48614  grimcnv  48636  uhgrimedgi  48638  isuspgrim0  48642  isuspgrimlem  48643  gricushgr  48665  clnbgrgrimlem  48681  clnbgrgrim  48682  grimedg  48683  grtrissvtx  48692  stgrusgra  48707  isubgr3stgrlem7  48720  gpgiedgdmellem  48794  gpgusgralem  48804  gpgvtxedg0  48811  gpgvtxedg1  48812  copisnmnd  48917  lidldomn1  48979  affinecomb1  49465  eenglngeehlnmlem2  49501  rrx2vlinest  49504  itsclquadb  49539  aacllem  50584