Theorem rexlimiv 2546

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

Syntax hints:   -> wi 4   e. wcel 1481   E.wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  rexlimiva  2547  rexlimivw  2548  rexlimivv  2558  r19.36av  2585  r19.44av  2593  r19.45av  2594  rexn0  3466  uniss2  3775  elres  4863  ssimaex  5490  tfrlem5  6219  tfrlem8  6223  ecoptocl  6524  mapsn  6592  elixpsn  6637  ixpsnf1o  6638  findcard  6790  findcard2  6791  findcard2s  6792  fiintim  6825  prnmaddl  7322  0re  7790  cnegexlem2  7962  0cnALT  7976  bndndx  9000  uzn0  9365  ublbneg  9432  rexanuz2  10795  opnneiid  12372  bj-inf2vnlem2  13340