Theorem rexlimiv 2608

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

Syntax hints:   -> wi 4   e. wcel 2167   E.wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  rexlimiva  2609  rexlimivw  2610  rexlimivv  2620  r19.36av  2648  r19.44av  2656  r19.45av  2657  rexn0  3550  uniss2  3871  elres  4983  ssimaex  5625  mpoexw  6280  tfrlem5  6381  tfrlem8  6385  ecoptocl  6690  mapsn  6758  elixpsn  6803  ixpsnf1o  6804  findcard  6958  findcard2  6959  findcard2s  6960  fiintim  7001  prnmaddl  7574  0re  8043  cnegexlem2  8219  0cnALT  8233  bndndx  9265  uzn0  9634  ublbneg  9704  rexanuz2  11173  opnneiid  14484  2lgslem1b  15414  2sqlem2  15440  bj-inf2vnlem2  15701