Theorem rexlimiv 2601

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 1539	. 2 |- F/ x ps
2		rexlimiv.1	. 2 |- ( x e. A -> ( ph -> ps ) )
3	1, 2	rexlimi 2600	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   e. wcel 2160   E.wrex 2469

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474

This theorem is referenced by:  rexlimiva  2602  rexlimivw  2603  rexlimivv  2613  r19.36av  2641  r19.44av  2649  r19.45av  2650  rexn0  3536  uniss2  3855  elres  4958  ssimaex  5593  mpoexw  6232  tfrlem5  6333  tfrlem8  6337  ecoptocl  6640  mapsn  6708  elixpsn  6753  ixpsnf1o  6754  findcard  6906  findcard2  6907  findcard2s  6908  fiintim  6946  prnmaddl  7507  0re  7975  cnegexlem2  8151  0cnALT  8165  bndndx  9193  uzn0  9561  ublbneg  9631  rexanuz2  11018  opnneiid  14061  2sqlem2  14859  bj-inf2vnlem2  15120