Theorem rexlimdv 2586

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

Ref	Expression
rexlimdv.1	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

Ref	Expression
rexlimdv	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		nfv 1521	. 2 |- F/ x ph
2		nfv 1521	. 2 |- F/ x ch
3		rexlimdv.1	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
4	1, 2, 3	rexlimd 2584	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 2141   E.wrex 2449

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  rexlimdva  2587  rexlimdv3a  2589  rexlimdva2  2590  rexlimdvw  2591  rexlimdvv  2594  ssorduni  4471  funcnvuni  5267  dffo3  5643  smoiun  6280  tfrlem9  6298  ordiso2  7012  axprecex  7842  recexap  8571  zdiv  9300  btwnz  9331  lbzbi  9575  neibl  13285  metcnp3  13305