Theorem rexlimiv 2654

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

Syntax hints:   -> wi 4   e. wcel 2203   E.wrex 2521

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 2525  df-rex 2526

This theorem is referenced by:  rexlimiva  2655  rexlimivw  2656  rexlimivv  2666  r19.36av  2694  r19.44av  2702  r19.45av  2703  rexn0  3608  uniss2  3945  elres  5074  ssimaex  5738  mpoexw  6409  tfrlem5  6545  tfrlem8  6549  ecoptocl  6856  mapsn  6925  elixpsn  6970  ixpsnf1o  6971  findcard  7145  findcard2  7146  findcard2s  7147  fiintim  7191  prnmaddl  7805  0re  8274  cnegexlem2  8449  0cnALT  8463  bndndx  9495  uzn0  9870  ublbneg  9945  rexanuz2  11676  opnneiid  15029  2lgslem1b  15962  2sqlem2  15988  bj-inf2vnlem2  16741