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  6003  tfri3  6532  mapxpen  7033  fodjuomnilemdc  7342  cc3  7486  zsupcllemstep  10488  fimaxre2  11787  fprodcllemf  12173  fprodap0f  12196  fprodle  12200  bezoutlemmain  12568  bezoutlemzz  12572  exmidunben  13046  mulcncf  15331  limccnp2lem  15399  lfgrnloopen  15983