Theorem rexlimdva 2622

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 115	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2621	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2175   E.wrex 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  rexlimdvaa  2623  rexlimivv  2628  rexlimdvv  2629  ralxfrd  4508  rexxfrd  4509  fvelimab  5634  foco2  5821  elunirn  5834  f1elima  5841  mpoexw  6298  tfrlem5  6399  tfrlemibacc  6411  tfrlemibfn  6413  tfr1onlembacc  6427  tfr1onlembfn  6429  tfrcllembacc  6440  tfrcllembfn  6442  frecabcl  6484  nnaordex  6613  nnawordex  6614  ectocld  6687  phpm  6961  dif1enen  6976  fin0  6981  fin0or  6982  fimax2gtri  6997  fidcenum  7057  suplub2ti  7102  supisoex  7110  enomnilem  7239  finomni  7241  enmkvlem  7262  exmidfodomrlemeldju  7306  exmidfodomrlemreseldju  7307  ltexnqq  7520  ltbtwnnqq  7527  prarloclem4  7610  prarloc2  7616  genprndl  7633  genprndu  7634  prmuloc2  7679  1idprl  7702  1idpru  7703  cauappcvgprlemdisj  7763  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  recexgt0sr  7885  map2psrprg  7917  suplocsrlem  7920  nntopi  8006  cnegexlem1  8246  cnegexlem2  8247  renegcl  8332  aptap  8722  supinfneg  9715  infsupneg  9716  qmulz  9743  elpq  9769  icc0r  10047  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  ioo0  10400  ico0  10402  ioc0  10403  modqmuladd  10509  addmodlteq  10541  frec2uzrand  10548  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  hashunlem  10947  shftlem  11098  caucvgre  11263  resqrexlemgt0  11302  rexico  11503  negfi  11510  climuni  11575  climshftlemg  11584  climcn1  11590  serf0  11634  summodclem2  11664  zsumdc  11666  fsum2dlemstep  11716  mertenslem2  11818  ntrivcvgap  11830  zproddc  11861  fprod2dlemstep  11904  dvds1lem  12084  odd2np1lem  12154  odd2np1  12155  sqoddm1div8z  12168  ltoddhalfle  12175  halfleoddlt  12176  m1expo  12182  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  flodddiv4  12218  bezoutlemaz  12295  bezoutlembz  12296  dvdssqim  12316  ncoprmgcdne1b  12382  coprmdvds2  12386  divgcdcoprm0  12394  cncongr1  12396  cncongr2  12397  dvdsnprmd  12418  rpexp  12446  pythagtriplem1  12559  pc2dvds  12624  difsqpwdvds  12632  oddprmdvds  12648  prmpwdvds  12649  4sqlem11  12695  imasmnd2  13255  dfgrp3mlem  13401  imasgrp2  13417  issubg4m  13500  imasabl  13643  ringinvnzdiv  13783  imasring  13797  dvdsrcl2  13832  dvdsrmul1  13835  isnzr2  13917  lss1d  14116  lssats2  14147  lspsn  14149  dvdsrzring  14336  znunit  14392  znrrg  14393  tgcl  14507  innei  14606  cnptoprest  14682  lmss  14689  lmtopcnp  14693  txlm  14722  blssps  14870  blss  14871  blssexps  14872  blssex  14873  mopni3  14927  metrest  14949  metcnp3  14954  mulc1cncf  15032  cncfco  15034  elply2  15178  gausslemma2dlem1a  15506  lgsquadlem1  15525  2lgsoddprmlem2  15554  subctctexmid  15899