Theorem rexlimiv 2645

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

Syntax hints:   -> wi 4   e. wcel 2202   E.wrex 2512

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 2516  df-rex 2517

This theorem is referenced by:  rexlimiva  2646  rexlimivw  2647  rexlimivv  2657  r19.36av  2685  r19.44av  2693  r19.45av  2694  rexn0  3595  uniss2  3929  elres  5055  ssimaex  5716  mpoexw  6387  tfrlem5  6523  tfrlem8  6527  ecoptocl  6834  mapsn  6902  elixpsn  6947  ixpsnf1o  6948  findcard  7120  findcard2  7121  findcard2s  7122  fiintim  7166  prnmaddl  7770  0re  8239  cnegexlem2  8414  0cnALT  8428  bndndx  9460  uzn0  9833  ublbneg  9908  rexanuz2  11631  opnneiid  14975  2lgslem1b  15908  2sqlem2  15934  bj-inf2vnlem2  16687