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  4996  ssimaex  5642  mpoexw  6301  tfrlem5  6402  tfrlem8  6406  ecoptocl  6711  mapsn  6779  elixpsn  6824  ixpsnf1o  6825  findcard  6987  findcard2  6988  findcard2s  6989  fiintim  7030  prnmaddl  7605  0re  8074  cnegexlem2  8250  0cnALT  8264  bndndx  9296  uzn0  9666  ublbneg  9736  rexanuz2  11335  opnneiid  14669  2lgslem1b  15599  2sqlem2  15625  bj-inf2vnlem2  15944