Theorem ralrimi 2541

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 1515	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2453	. 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 1346   F/wnf 1453   e. wcel 2141   A.wral 2448

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 1440  ax-gen 1442  ax-4 1503

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralrimiv  2542  reximdai  2568  r19.12  2576  rexlimd  2584  rexlimd2  2585  r19.29af2  2610  r19.37  2622  ralidm  3515  iineq2d  3893  mpteq2da  4078  onintonm  4501  mpteqb  5586  fmptdf  5653  eusvobj2  5839  tfri3  6346  mapxpen  6826  fodjuomnilemdc  7120  cc3  7230  fimaxre2  11190  fprodcllemf  11576  fprodap0f  11599  fprodle  11603  zsupcllemstep  11900  bezoutlemmain  11953  bezoutlemzz  11957  exmidunben  12381  mulcncf  13385  limccnp2lem  13439