Theorem ralrimi 2528

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 1502	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2440	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
5	3, 4	sylibr 133	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   A.wal 1333   F/wnf 1440   e. wcel 2128   A.wral 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440

This theorem is referenced by:  ralrimiv  2529  reximdai  2555  r19.12  2563  rexlimd  2571  rexlimd2  2572  r19.29af2  2597  r19.37  2609  ralidm  3495  iineq2d  3871  mpteq2da  4055  onintonm  4478  mpteqb  5560  fmptdf  5626  eusvobj2  5812  tfri3  6316  mapxpen  6795  fodjuomnilemdc  7089  cc3  7190  fimaxre2  11137  fprodcllemf  11521  fprodap0f  11544  fprodle  11548  zsupcllemstep  11844  bezoutlemmain  11897  bezoutlemzz  11901  exmidunben  12225  mulcncf  13061  limccnp2lem  13115