Theorem ralrimi 2579

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)

Hypotheses

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

Assertion

Ref	Expression
ralrimi	|- ( ph -> A. x e. A ps )

Proof of Theorem ralrimi

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 |- F/ x ph
2		ralrimi.2	. . 3 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	alrimi 1546	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2491	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
5	3, 4	sylibr 134	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   A.wal 1371   F/wnf 1484   e. wcel 2178   A.wral 2486

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 1471  ax-gen 1473  ax-4 1534

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  ralrimiv  2580  reximdai  2606  r19.12  2614  rexlimd  2622  rexlimd2  2623  r19.29af2  2648  r19.37  2660  ralidm  3569  iineq2d  3961  mpteq2da  4149  onintonm  4583  mpteqb  5693  fmptdf  5760  eusvobj2  5953  tfri3  6476  mapxpen  6970  fodjuomnilemdc  7272  cc3  7415  zsupcllemstep  10409  fimaxre2  11653  fprodcllemf  12039  fprodap0f  12062  fprodle  12066  bezoutlemmain  12434  bezoutlemzz  12438  exmidunben  12912  mulcncf  15195  limccnp2lem  15263  lfgrnloopen  15839