Theorem ralrimiv 2542

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

Syntax hints:   -> wi 4   e. wcel 2141   A.wral 2448

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralrimiva  2543  ralrimivw  2544  ralrimivv  2551  r19.27av  2605  rr19.3v  2869  rabssdv  3227  rzal  3512  trin  4097  class2seteq  4149  ralxfrALT  4452  ssorduni  4471  ordsucim  4484  onintonm  4501  issref  4993  funimaexglem  5281  resflem  5660  poxp  6211  rdgss  6362  dom2lem  6750  supisoti  6987  ordiso2  7012  updjud  7059  uzind  9323  zindd  9330  lbzbi  9575  icoshftf1o  9948  maxabslemval  11172  xrmaxiflemval  11213  fisum0diag2  11410  alzdvds  11814  hashgcdeq  12193  tgcl  12858  distop  12879  neiuni  12955  cnpnei  13013  isxmetd  13141  fsumcncntop  13350  bj-nntrans2  13987  bj-inf2vnlem1  14005