Theorem rexlimdv 2613

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

Syntax hints:   -> wi 4   e. wcel 2167   E.wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  rexlimdva  2614  rexlimdv3a  2616  rexlimdva2  2617  rexlimdvw  2618  rexlimdvv  2621  ssorduni  4524  funcnvuni  5328  dffo3  5712  smoiun  6368  tfrlem9  6386  ordiso2  7110  axprecex  7964  recexap  8697  zdiv  9431  btwnz  9462  lbzbi  9707  imasmnd2  13154  imasgrp2  13316  imasrng  13588  imasring  13696  neibl  14811  metcnp3  14831