Theorem rexlimiv 2619

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

Syntax hints:   -> wi 4   e. wcel 2178   E.wrex 2487

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  rexlimiva  2620  rexlimivw  2621  rexlimivv  2631  r19.36av  2659  r19.44av  2667  r19.45av  2668  rexn0  3567  uniss2  3895  elres  5014  ssimaex  5663  mpoexw  6322  tfrlem5  6423  tfrlem8  6427  ecoptocl  6732  mapsn  6800  elixpsn  6845  ixpsnf1o  6846  findcard  7011  findcard2  7012  findcard2s  7013  fiintim  7054  prnmaddl  7638  0re  8107  cnegexlem2  8283  0cnALT  8297  bndndx  9329  uzn0  9699  ublbneg  9769  rexanuz2  11417  opnneiid  14751  2lgslem1b  15681  2sqlem2  15707  bj-inf2vnlem2  16106