Theorem ralrimi 2615

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 2527	. 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 2205   A.wral 2522

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 2527

This theorem is referenced by:  ralrimiv  2616  reximdai  2642  r19.12  2651  rexlimd  2659  rexlimd2  2660  r19.29af2  2685  r19.37  2697  ralidm  3614  iineq2d  4016  mpteq2da  4204  onintonm  4644  mpteqb  5773  fmptdf  5839  eusvobj2  6044  funimass4f  6332  tfri3  6611  mapxpen  7114  fodjuomnilemdc  7448  cc3  7598  zsupcllemstep  10611  fimaxre2  11937  fprodcllemf  12324  fprodap0f  12347  fprodle  12351  bezoutlemmain  12719  bezoutlemzz  12723  exmidunben  13261  mulcncf  15599  limccnp2lem  15667  lfgrnloopen  16254