Theorem rexlimiv 2656

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

Syntax hints:   -> wi 4   e. wcel 2205   E.wrex 2523

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527  df-rex 2528

This theorem is referenced by:  rexlimiva  2657  rexlimivw  2658  rexlimivv  2668  r19.36av  2696  r19.44av  2704  r19.45av  2705  rexn0  3612  uniss2  3950  elres  5079  ssimaex  5743  mpoexw  6422  tfrlem5  6558  tfrlem8  6562  ecoptocl  6869  mapsn  6938  elixpsn  6983  ixpsnf1o  6984  findcard  7158  findcard2  7159  findcard2s  7160  fiintim  7204  prnmaddl  7821  0re  8290  cnegexlem2  8465  0cnALT  8479  bndndx  9512  uzn0  9888  ublbneg  9963  rexanuz2  11701  opnneiid  15155  2lgslem1b  16088  2sqlem2  16114  bj-inf2vnlem2  16867