Theorem rexlimdv 2738

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

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:  rexlimdva  2739  rexlimdv3a  2741  rexlimdvw  2742  rexlimdvv  2745  eqpw1uni  4331  nndisjeq  4430  ssfin  4471  nnpw1ex  4485  tfinltfinlem1  4501  sfin112  4530  sfintfin  4533  sfinltfin  4536  funcnvuni  5162  dffo3  5423  nclenn  6250  ncslesuc  6268