Theorem rexlimiv 2733

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

Syntax hints:   -> wi 4   e. wcel 1710  E.wrex 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2620  df-rex 2621

This theorem is referenced by:  rexlimiva  2734  rexlimivw  2735  rexlimivv  2744  r19.36av  2760  r19.44av  2768  r19.45av  2769  rexn0  3653  uniss2  3923  pwadjoin  4120  nnc0suc  4413  lefinlteq  4464  ssfin  4471  evennn  4507  oddnn  4508  sucoddeven  4512  evenodddisj  4517  eventfin  4518  oddtfin  4519  fnasrn  5418  ecoptocl  5997  mapsn  6027  dflec3  6222  lenc  6224  taddc  6230  ce0tb  6239  ce0lenc1  6240  ncfin  6248  nncdiv3  6278  nchoicelem1  6290  nchoicelem2  6291  nchoicelem12  6301