Theorem ralrimi 2568

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 1536	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2480	. 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 1474   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463  ax-4 1524

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralrimiv  2569  reximdai  2595  r19.12  2603  rexlimd  2611  rexlimd2  2612  r19.29af2  2637  r19.37  2649  ralidm  3552  iineq2d  3937  mpteq2da  4123  onintonm  4554  mpteqb  5655  fmptdf  5722  eusvobj2  5911  tfri3  6434  mapxpen  6918  fodjuomnilemdc  7219  cc3  7351  zsupcllemstep  10336  fimaxre2  11409  fprodcllemf  11795  fprodap0f  11818  fprodle  11822  bezoutlemmain  12190  bezoutlemzz  12194  exmidunben  12668  mulcncf  14928  limccnp2lem  14996