Theorem ralrimi 2621

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 1575	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2533	. 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 1400   F/wnf 1513   e. wcel 2209   A.wral 2528

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 1500  ax-gen 1502  ax-4 1563

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  ralrimiv  2622  reximdai  2648  r19.12  2657  rexlimd  2665  rexlimd2  2666  r19.29af2  2691  r19.37  2703  ralidm  3625  iineq2d  4027  mpteq2da  4215  onintonm  4659  mpteqb  5790  fmptdf  5856  eusvobj2  6061  funimass4f  6349  tfri3  6628  mapxpen  7138  fodjuomnilemdc  7474  cc3  7624  zsupcllemstep  10640  fimaxre2  11971  fprodcllemf  12358  fprodap0f  12381  fprodle  12385  bezoutlemmain  12753  bezoutlemzz  12757  exmidunben  13295  mulcncf  15632  limccnp2lem  15700  lfgrnloopen  16288