Theorem ralrimi 2537

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 1510	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2449	. 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 1341   F/wnf 1448   e. wcel 2136   A.wral 2444

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 1435  ax-gen 1437  ax-4 1498

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralrimiv  2538  reximdai  2564  r19.12  2572  rexlimd  2580  rexlimd2  2581  r19.29af2  2606  r19.37  2618  ralidm  3509  iineq2d  3886  mpteq2da  4071  onintonm  4494  mpteqb  5576  fmptdf  5642  eusvobj2  5828  tfri3  6335  mapxpen  6814  fodjuomnilemdc  7108  cc3  7209  fimaxre2  11168  fprodcllemf  11554  fprodap0f  11577  fprodle  11581  zsupcllemstep  11878  bezoutlemmain  11931  bezoutlemzz  11935  exmidunben  12359  mulcncf  13241  limccnp2lem  13295