Theorem rexlimdv 2593

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 1528	. 2 |- F/ x ph
2		nfv 1528	. 2 |- F/ x ch
3		rexlimdv.1	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
4	1, 2, 3	rexlimd 2591	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 2148   E.wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  rexlimdva  2594  rexlimdv3a  2596  rexlimdva2  2597  rexlimdvw  2598  rexlimdvv  2601  ssorduni  4488  funcnvuni  5287  dffo3  5665  smoiun  6304  tfrlem9  6322  ordiso2  7036  axprecex  7881  recexap  8612  zdiv  9343  btwnz  9374  lbzbi  9618  neibl  14076  metcnp3  14096