Theorem ralrimi 2603

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 1570	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2515	. 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 1395   F/wnf 1508   e. wcel 2202   A.wral 2510

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 1495  ax-gen 1497  ax-4 1558

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralrimiv  2604  reximdai  2630  r19.12  2639  rexlimd  2647  rexlimd2  2648  r19.29af2  2673  r19.37  2685  ralidm  3595  iineq2d  3990  mpteq2da  4178  onintonm  4615  mpteqb  5737  fmptdf  5804  eusvobj2  6004  tfri3  6533  mapxpen  7034  fodjuomnilemdc  7343  cc3  7487  zsupcllemstep  10490  fimaxre2  11805  fprodcllemf  12192  fprodap0f  12215  fprodle  12219  bezoutlemmain  12587  bezoutlemzz  12591  exmidunben  13065  mulcncf  15351  limccnp2lem  15419  lfgrnloopen  16003