Theorem ralrimi 2604

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 1571	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2516	. 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 1396   F/wnf 1509   e. wcel 2202   A.wral 2511

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 1496  ax-gen 1498  ax-4 1559

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  ralrimiv  2605  reximdai  2631  r19.12  2640  rexlimd  2648  rexlimd2  2649  r19.29af2  2674  r19.37  2686  ralidm  3597  iineq2d  3995  mpteq2da  4183  onintonm  4621  mpteqb  5746  fmptdf  5812  eusvobj2  6014  tfri3  6576  mapxpen  7077  fodjuomnilemdc  7386  cc3  7530  zsupcllemstep  10535  fimaxre2  11850  fprodcllemf  12237  fprodap0f  12260  fprodle  12264  bezoutlemmain  12632  bezoutlemzz  12636  exmidunben  13110  mulcncf  15402  limccnp2lem  15470  lfgrnloopen  16057