Theorem rexlimd 2833

Description: Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Hypotheses

Ref	Expression
rexlimd.1	|- F/ x ph
rexlimd.2	|- F/ x ch
rexlimd.3	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

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

Proof of Theorem rexlimd

Step	Hyp	Ref	Expression
1		rexlimd.1	. . 3 |- F/ x ph
2		rexlimd.3	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	1, 2	ralrimi 2792	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
4		rexlimd.2	. . 3 |- F/ x ch
5	4	r19.23 2827	. 2 |- ( A. x e. A ( ps -> ch ) <-> ( E. x e. A ps -> ch ) )
6	3, 5	sylib 196	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   F/wnf 1589   e. wcel 1756   A.wral 2710   E.wrex 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716

This theorem is referenced by:  rexlimdv  2835  reusv2lem2  4489  reusv6OLD  4498  ralxfrALT  4506  fvmptt  5784  ffnfv  5864  peano5  6494  tz7.49  6892  nneneq  7486  ac6sfi  7548  ixpiunwdom  7798  r1val1  7985  rankuni2b  8052  infpssrlem4  8467  zorn2lem4  8660  zorn2lem5  8661  konigthlem  8724  tskuni  8942  gruiin  8969  lbzbi  10935  iunconlem  19006  ptbasfi  19129  alexsubALTlem3  19596  ovoliunnul  20965  iunmbl2  21013  mptelee  23092  atom1d  25708  elabreximd  25842  iundisjf  25882  esumc  26457  heicant  28379  indexa  28580  sdclem2  28591  refsumcn  29705  fmul01lt1  29720  stoweidlem29  29777  stoweidlem31  29779  stoweidlem59  29807  stirlinglem13  29834  ffnafv  30030  glbconxN  32862  cdleme26ee  33844  cdleme32d  33928  cdleme32f  33930  cdlemk38  34399  cdlemk19x  34427  cdlemk11t  34430