Theorem ralrimi 2503

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 1502	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2421	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
5	3, 4	sylibr 133	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   A.wal 1329   F/wnf 1436   e. wcel 1480   A.wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralrimiv  2504  reximdai  2530  r19.12  2538  rexlimd  2546  rexlimd2  2547  r19.29af2  2572  r19.37  2583  ralidm  3463  iineq2d  3833  mpteq2da  4017  onintonm  4433  mpteqb  5511  fmptdf  5577  eusvobj2  5760  tfri3  6264  mapxpen  6742  fodjuomnilemdc  7016  fimaxre2  10998  zsupcllemstep  11638  bezoutlemmain  11686  bezoutlemzz  11690  exmidunben  11939  mulcncf  12760  limccnp2lem  12814