Theorem ralrimi 2433

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 1456	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2354	. 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 1283   F/wnf 1390   e. wcel 1434   A.wral 2349

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 1377  ax-gen 1379  ax-4 1441

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354

This theorem is referenced by:  ralrimiv  2434  reximdai  2460  r19.12  2467  rexlimd  2475  rexlimd2  2476  r19.29af2  2497  r19.37  2507  ralidm  3349  iineq2d  3706  mpteq2da  3875  onintonm  4269  mpteqb  5293  eusvobj2  5529  tfri3  6016  fimaxre2  10247  zsupcllemstep  10485  bezoutlemmain  10531  bezoutlemzz  10535