Theorem ralrimi 2561

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 1533	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2473	. 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 1362   F/wnf 1471   e. wcel 2160   A.wral 2468

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 1458  ax-gen 1460  ax-4 1521

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  ralrimiv  2562  reximdai  2588  r19.12  2596  rexlimd  2604  rexlimd2  2605  r19.29af2  2630  r19.37  2642  ralidm  3538  iineq2d  3921  mpteq2da  4107  onintonm  4534  mpteqb  5626  fmptdf  5693  eusvobj2  5881  tfri3  6391  mapxpen  6875  fodjuomnilemdc  7171  cc3  7296  fimaxre2  11266  fprodcllemf  11652  fprodap0f  11675  fprodle  11679  zsupcllemstep  11977  bezoutlemmain  12030  bezoutlemzz  12034  exmidunben  12476  mulcncf  14543  limccnp2lem  14597