Theorem ralrimi 2613

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 2525	. 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 2203   A.wral 2520

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 2525

This theorem is referenced by:  ralrimiv  2614  reximdai  2640  r19.12  2649  rexlimd  2657  rexlimd2  2658  r19.29af2  2683  r19.37  2695  ralidm  3610  iineq2d  4011  mpteq2da  4199  onintonm  4639  mpteqb  5768  fmptdf  5834  eusvobj2  6036  tfri3  6598  mapxpen  7101  fodjuomnilemdc  7435  cc3  7582  zsupcllemstep  10589  fimaxre2  11912  fprodcllemf  12299  fprodap0f  12322  fprodle  12326  bezoutlemmain  12694  bezoutlemzz  12698  exmidunben  13177  mulcncf  15473  limccnp2lem  15541  lfgrnloopen  16128