Theorem ralrimiv 2529

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 1508	. 2 |- F/ x ph
2		ralrimiv.1	. 2 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	ralrimi 2528	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2128   A.wral 2435

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440

This theorem is referenced by:  ralrimiva  2530  ralrimivw  2531  ralrimivv  2538  r19.27av  2592  rr19.3v  2851  rabssdv  3208  rzal  3491  trin  4072  class2seteq  4124  ralxfrALT  4427  ssorduni  4446  ordsucim  4459  onintonm  4476  issref  4968  funimaexglem  5253  resflem  5631  poxp  6179  rdgss  6330  dom2lem  6717  supisoti  6954  ordiso2  6979  updjud  7026  uzind  9275  zindd  9282  lbzbi  9525  icoshftf1o  9895  maxabslemval  11108  xrmaxiflemval  11147  fisum0diag2  11344  alzdvds  11746  hashgcdeq  12114  tgcl  12475  distop  12496  neiuni  12572  cnpnei  12630  isxmetd  12758  fsumcncntop  12967  bj-nntrans2  13538  bj-inf2vnlem1  13556