Theorem rexlimdva 2587

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
rexlimdva	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 114	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2586	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2141   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  rexlimdvaa  2588  rexlimivv  2593  rexlimdvv  2594  ralxfrd  4447  rexxfrd  4448  fvelimab  5552  foco2  5733  elunirn  5745  f1elima  5752  mpoexw  6192  tfrlem5  6293  tfrlemibacc  6305  tfrlemibfn  6307  tfr1onlembacc  6321  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembfn  6336  frecabcl  6378  nnaordex  6507  nnawordex  6508  ectocld  6579  phpm  6843  dif1enen  6858  fin0  6863  fin0or  6864  fimax2gtri  6879  fidcenum  6933  suplub2ti  6978  supisoex  6986  enomnilem  7114  finomni  7116  enmkvlem  7137  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  ltexnqq  7370  ltbtwnnqq  7377  prarloclem4  7460  prarloc2  7466  genprndl  7483  genprndu  7484  prmuloc2  7529  1idprl  7552  1idpru  7553  cauappcvgprlemdisj  7613  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  recexgt0sr  7735  map2psrprg  7767  suplocsrlem  7770  nntopi  7856  cnegexlem1  8094  cnegexlem2  8095  renegcl  8180  supinfneg  9554  infsupneg  9555  qmulz  9582  elpq  9607  icc0r  9883  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  ioo0  10216  ico0  10218  ioc0  10219  modqmuladd  10322  addmodlteq  10354  frec2uzrand  10361  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  hashunlem  10739  shftlem  10780  caucvgre  10945  resqrexlemgt0  10984  rexico  11185  negfi  11191  climuni  11256  climshftlemg  11265  climcn1  11271  serf0  11315  summodclem2  11345  zsumdc  11347  fsum2dlemstep  11397  mertenslem2  11499  ntrivcvgap  11511  zproddc  11542  fprod2dlemstep  11585  dvds1lem  11764  odd2np1lem  11831  odd2np1  11832  sqoddm1div8z  11845  ltoddhalfle  11852  halfleoddlt  11853  m1expo  11859  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  flodddiv4  11893  bezoutlemaz  11958  bezoutlembz  11959  dvdssqim  11979  ncoprmgcdne1b  12043  coprmdvds2  12047  divgcdcoprm0  12055  cncongr1  12057  cncongr2  12058  dvdsnprmd  12079  rpexp  12107  pythagtriplem1  12219  pc2dvds  12283  difsqpwdvds  12291  oddprmdvds  12306  prmpwdvds  12307  tgcl  12858  innei  12957  cnptoprest  13033  lmss  13040  lmtopcnp  13044  txlm  13073  blssps  13221  blss  13222  blssexps  13223  blssex  13224  mopni3  13278  metrest  13300  metcnp3  13305  mulc1cncf  13370  cncfco  13372  subctctexmid  14034