Theorem rexlimdv 2647

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

Syntax hints:   -> wi 4   e. wcel 2200   E.wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexlimdva  2648  rexlimdv3a  2650  rexlimdva2  2651  rexlimdvw  2652  rexlimdvv  2655  ssorduni  4579  funcnvuni  5390  dffo3  5784  smoiun  6453  tfrlem9  6471  ordiso2  7213  axprecex  8078  recexap  8811  zdiv  9546  btwnz  9577  lbzbi  9823  imasmnd2  13501  imasgrp2  13663  imasrng  13935  imasring  14043  neibl  15181  metcnp3  15201  ushgredgedg  16040  ushgredgedgloop  16042