Theorem rexlimiv 2605

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 2604	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   e. wcel 2164   E.wrex 2473

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 2477  df-rex 2478

This theorem is referenced by:  rexlimiva  2606  rexlimivw  2607  rexlimivv  2617  r19.36av  2645  r19.44av  2653  r19.45av  2654  rexn0  3546  uniss2  3867  elres  4979  ssimaex  5619  mpoexw  6268  tfrlem5  6369  tfrlem8  6373  ecoptocl  6678  mapsn  6746  elixpsn  6791  ixpsnf1o  6792  findcard  6946  findcard2  6947  findcard2s  6948  fiintim  6987  prnmaddl  7552  0re  8021  cnegexlem2  8197  0cnALT  8211  bndndx  9242  uzn0  9611  ublbneg  9681  rexanuz2  11138  opnneiid  14343  2lgslem1b  15246  2sqlem2  15272  bj-inf2vnlem2  15533