Theorem ralrimi 2444

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

Syntax hints:   -> wi 4   A.wal 1287   F/wnf 1394   e. wcel 1438   A.wral 2359

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364

This theorem is referenced by:  ralrimiv  2445  reximdai  2471  r19.12  2478  rexlimd  2486  rexlimd2  2487  r19.29af2  2508  r19.37  2519  ralidm  3378  iineq2d  3745  mpteq2da  3919  onintonm  4324  mpteqb  5377  fmptdf  5439  eusvobj2  5620  tfri3  6114  mapxpen  6544  fodjuomnilemdc  6778  fimaxre2  10622  zsupcllemstep  11023  bezoutlemmain  11069  bezoutlemzz  11073