Theorem ralrimiv 2507

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

Syntax hints:   -> wi 4   e. wcel 1481   A.wral 2417

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  ralrimiva  2508  ralrimivw  2509  ralrimivv  2516  r19.27av  2570  rr19.3v  2827  rabssdv  3182  rzal  3465  trin  4044  class2seteq  4095  ralxfrALT  4396  ssorduni  4411  ordsucim  4424  onintonm  4441  issref  4929  funimaexglem  5214  resflem  5592  poxp  6137  rdgss  6288  dom2lem  6674  supisoti  6905  ordiso2  6928  updjud  6975  uzind  9186  zindd  9193  lbzbi  9435  icoshftf1o  9804  maxabslemval  11012  xrmaxiflemval  11051  fisum0diag2  11248  alzdvds  11588  hashgcdeq  11940  tgcl  12272  distop  12293  neiuni  12369  cnpnei  12427  isxmetd  12555  fsumcncntop  12764  bj-nntrans2  13321  bj-inf2vnlem1  13339