Theorem rexlimd 2937

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 2818	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
4		rexlimd.2	. . 3 |- F/ x ch
5	4	r19.23 2931	. 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 1590   e. wcel 1758   A.wral 2795   E.wrex 2796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2800  df-rex 2801

This theorem is referenced by:  rexlimdv  2939  reusv2lem2  4595  reusv6OLD  4604  ralxfrALT  4612  fvmptt  5891  ffnfv  5971  peano5  6602  tz7.49  7003  nneneq  7597  ac6sfi  7660  ixpiunwdom  7910  r1val1  8097  rankuni2b  8164  infpssrlem4  8579  zorn2lem4  8772  zorn2lem5  8773  konigthlem  8836  tskuni  9054  gruiin  9081  lbzbi  11047  iunconlem  19156  ptbasfi  19279  alexsubALTlem3  19746  ovoliunnul  21115  iunmbl2  21164  mptelee  23286  atom1d  25902  elabreximd  26036  iundisjf  26075  esumc  26643  heicant  28567  indexa  28768  sdclem2  28779  refsumcn  29893  fmul01lt1  29908  stoweidlem29  29965  stoweidlem31  29967  stoweidlem59  29995  stirlinglem13  30022  ffnafv  30218  glbconxN  33331  cdleme26ee  34313  cdleme32d  34397  cdleme32f  34399  cdlemk38  34868  cdlemk19x  34896  cdlemk11t  34899