Theorem rexlimdva 2433

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

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312

This theorem is referenced by:  rexlimdvaa  2434  rexlimivv  2438  rexlimdvv  2439  ralxfrd  4194  rexxfrd  4195  fvelimab  5229  foco2  5318  elunirn  5405  f1elima  5412  tfrlem5  5930  tfrlemibacc  5940  tfrlemibfn  5942  nnaordex  6100  nnawordex  6101  ectocld  6172  phpm  6327  fin0  6342  fin0or  6343  ltexnqq  6506  ltbtwnnqq  6513  prarloclem4  6596  prarloc2  6602  genprndl  6619  genprndu  6620  prmuloc2  6665  1idprl  6688  1idpru  6689  cauappcvgprlemdisj  6749  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  recexgt0sr  6858  nntopi  6968  cnegexlem1  7186  cnegexlem2  7187  renegcl  7272  qmulz  8558  icc0r  8795  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  frec2uzrand  9191  frecuzrdgfn  9198  shftlem  9417  caucvgre  9580  resqrexlemgt0  9618  climuni  9814  climshftlemg  9823  climcn1  9829  serif0  9871