Theorem ralrimi 2568

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 1536	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2480	. 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 1362   F/wnf 1474   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463  ax-4 1524

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralrimiv  2569  reximdai  2595  r19.12  2603  rexlimd  2611  rexlimd2  2612  r19.29af2  2637  r19.37  2649  ralidm  3552  iineq2d  3937  mpteq2da  4123  onintonm  4554  mpteqb  5653  fmptdf  5720  eusvobj2  5909  tfri3  6426  mapxpen  6910  fodjuomnilemdc  7211  cc3  7337  zsupcllemstep  10321  fimaxre2  11394  fprodcllemf  11780  fprodap0f  11803  fprodle  11807  bezoutlemmain  12175  bezoutlemzz  12179  exmidunben  12653  mulcncf  14854  limccnp2lem  14922