Theorem ralrimi 2506

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

Syntax hints:   -> wi 4   A.wal 1330   F/wnf 1437   e. wcel 1481   A.wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  ralrimiv  2507  reximdai  2533  r19.12  2541  rexlimd  2549  rexlimd2  2550  r19.29af2  2575  r19.37  2586  ralidm  3468  iineq2d  3841  mpteq2da  4025  onintonm  4441  mpteqb  5519  fmptdf  5585  eusvobj2  5768  tfri3  6272  mapxpen  6750  fodjuomnilemdc  7024  cc3  7100  fimaxre2  11030  zsupcllemstep  11674  bezoutlemmain  11722  bezoutlemzz  11726  exmidunben  11975  mulcncf  12799  limccnp2lem  12853