Theorem ralrimiv 2433

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)

Hypothesis

Ref	Expression
ralrimiv.1	|- ( ph -> ( x e. A -> ps ) )

Assertion

Ref	Expression
ralrimiv	|- ( ph -> A. x e. A ps )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem ralrimiv

Step	Hyp	Ref	Expression
1		nfv 1461	. 2 |- F/ x ph
2		ralrimiv.1	. 2 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	ralrimi 2432	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1433   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  ralrimiva  2434  ralrimivw  2435  ralrimivv  2442  r19.27av  2492  rr19.3v  2733  rabssdv  3074  rzal  3338  trin  3885  class2seteq  3937  ralxfrALT  4217  ssorduni  4231  ordsucim  4244  onintonm  4261  issref  4727  funimaexglem  5002  poxp  5873  rdgss  5993  dom2lem  6275  supisoti  6423  ordiso2  6446  uzind  8458  zindd  8465  lbzbi  8701  icoshftf1o  9013  maxabslemval  10094  alzdvds  10254  bj-nntrans2  10747  bj-inf2vnlem1  10765