Theorem rexlimd 2947

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.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)

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	. 2 |- F/ x ph
2		rexlimd.2	. . 3 |- F/ x ch
3	2	a1i 11	. 2 |- ( ph -> F/ x ch )
4		rexlimd.3	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
5	1, 3, 4	rexlimd2 2946	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   F/wnf 1599   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820

This theorem is referenced by:  rexlimdvOLD  2954  reusv2lem2  4649  reusv6OLD  4658  ralxfrALT  4666  fvmptt  5963  ffnfv  6045  peano5  6701  tz7.49  7107  nneneq  7697  ac6sfi  7760  ixpiunwdom  8013  r1val1  8200  rankuni2b  8267  infpssrlem4  8682  zorn2lem4  8875  zorn2lem5  8876  konigthlem  8939  tskuni  9157  gruiin  9184  lbzbi  11166  iunconlem  19694  ptbasfi  19817  alexsubALTlem3  20284  ovoliunnul  21653  iunmbl2  21702  mptelee  23874  atom1d  26948  elabreximd  27082  iundisjf  27121  esumc  27702  heicant  29626  indexa  29827  sdclem2  29838  refsumcn  30983  suprnmpt  31029  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  fmul01lt1  31136  islptre  31161  rexlim2d  31167  limcperiod  31170  islpcn  31181  limclner  31193  dvbdfbdioolem1  31258  itgiccshift  31298  itgperiod  31299  stoweidlem29  31329  stoweidlem31  31331  stoweidlem59  31359  stirlinglem13  31386  fourierdlem48  31455  fourierdlem51  31458  fourierdlem53  31460  fourierdlem80  31487  fourierdlem81  31488  fourierdlem93  31500  ffnafv  31723  glbconxN  34174  cdleme26ee  35156  cdleme32d  35240  cdleme32f  35242  cdlemk38  35711  cdlemk19x  35739  cdlemk11t  35742