Theorem rexlimiv 2581

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

Syntax hints:   -> wi 4   e. wcel 2141   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  rexlimiva  2582  rexlimivw  2583  rexlimivv  2593  r19.36av  2621  r19.44av  2629  r19.45av  2630  rexn0  3513  uniss2  3827  elres  4927  ssimaex  5557  mpoexw  6192  tfrlem5  6293  tfrlem8  6297  ecoptocl  6600  mapsn  6668  elixpsn  6713  ixpsnf1o  6714  findcard  6866  findcard2  6867  findcard2s  6868  fiintim  6906  prnmaddl  7452  0re  7920  cnegexlem2  8095  0cnALT  8109  bndndx  9134  uzn0  9502  ublbneg  9572  rexanuz2  10955  opnneiid  12958  2sqlem2  13745  bj-inf2vnlem2  14006