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  3551  iineq2d  3936  mpteq2da  4122  onintonm  4553  mpteqb  5652  fmptdf  5719  eusvobj2  5908  tfri3  6425  mapxpen  6909  fodjuomnilemdc  7210  cc3  7335  zsupcllemstep  10319  fimaxre2  11392  fprodcllemf  11778  fprodap0f  11801  fprodle  11805  bezoutlemmain  12165  bezoutlemzz  12169  exmidunben  12643  mulcncf  14844  limccnp2lem  14912