Theorem rexlimiv 2617

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

Syntax hints:   -> wi 4   e. wcel 2176   E.wrex 2485

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  rexlimiva  2618  rexlimivw  2619  rexlimivv  2629  r19.36av  2657  r19.44av  2665  r19.45av  2666  rexn0  3559  uniss2  3881  elres  4995  ssimaex  5640  mpoexw  6299  tfrlem5  6400  tfrlem8  6404  ecoptocl  6709  mapsn  6777  elixpsn  6822  ixpsnf1o  6823  findcard  6985  findcard2  6986  findcard2s  6987  fiintim  7028  prnmaddl  7603  0re  8072  cnegexlem2  8248  0cnALT  8262  bndndx  9294  uzn0  9664  ublbneg  9734  rexanuz2  11302  opnneiid  14636  2lgslem1b  15566  2sqlem2  15592  bj-inf2vnlem2  15907