Theorem rexlimiv 2471

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
rexlimiv.1	|- ( x e. A -> ( ph -> ps ) )

Assertion

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

Distinct variable group:   ps, x

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

Proof of Theorem rexlimiv

Step	Hyp	Ref	Expression
1		nfv 1461	. 2 |- F/ x ps
2		rexlimiv.1	. 2 |- ( x e. A -> ( ph -> ps ) )
3	1, 2	rexlimi 2470	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   e. wcel 1433   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353  df-rex 2354

This theorem is referenced by:  rexlimiva  2472  rexlimivw  2473  rexlimivv  2482  r19.36av  2505  r19.44av  2513  r19.45av  2514  rexn0  3339  uniss2  3632  elres  4664  ssimaex  5255  tfrlem5  5953  tfrlem8  5957  ecoptocl  6216  findcard  6372  findcard2  6373  findcard2s  6374  prnmaddl  6680  0re  7119  cnegexlem2  7284  0cnALT  7298  bndndx  8287  uzn0  8634  ublbneg  8698  rexanuz2  9877  bj-inf2vnlem2  10766