Theorem ralrimi 2565

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 1533	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2477	. 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 1471   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460  ax-4 1521

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralrimiv  2566  reximdai  2592  r19.12  2600  rexlimd  2608  rexlimd2  2609  r19.29af2  2634  r19.37  2646  ralidm  3547  iineq2d  3932  mpteq2da  4118  onintonm  4549  mpteqb  5648  fmptdf  5715  eusvobj2  5904  tfri3  6420  mapxpen  6904  fodjuomnilemdc  7203  cc3  7328  fimaxre2  11370  fprodcllemf  11756  fprodap0f  11779  fprodle  11783  zsupcllemstep  12082  bezoutlemmain  12135  bezoutlemzz  12139  exmidunben  12583  mulcncf  14762  limccnp2lem  14830