Theorem ralrimi 2548

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 1522	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2460	. 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 1351   F/wnf 1460   e. wcel 2148   A.wral 2455

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 1447  ax-gen 1449  ax-4 1510

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralrimiv  2549  reximdai  2575  r19.12  2583  rexlimd  2591  rexlimd2  2592  r19.29af2  2617  r19.37  2629  ralidm  3525  iineq2d  3908  mpteq2da  4094  onintonm  4518  mpteqb  5608  fmptdf  5675  eusvobj2  5863  tfri3  6370  mapxpen  6850  fodjuomnilemdc  7144  cc3  7269  fimaxre2  11237  fprodcllemf  11623  fprodap0f  11646  fprodle  11650  zsupcllemstep  11948  bezoutlemmain  12001  bezoutlemzz  12005  exmidunben  12429  mulcncf  14176  limccnp2lem  14230