Theorem ralrimiv 2538

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

Syntax hints:   -> wi 4   e. wcel 2136   A.wral 2444

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralrimiva  2539  ralrimivw  2540  ralrimivv  2547  r19.27av  2601  rr19.3v  2865  rabssdv  3222  rzal  3506  trin  4090  class2seteq  4142  ralxfrALT  4445  ssorduni  4464  ordsucim  4477  onintonm  4494  issref  4986  funimaexglem  5271  resflem  5649  poxp  6200  rdgss  6351  dom2lem  6738  supisoti  6975  ordiso2  7000  updjud  7047  uzind  9302  zindd  9309  lbzbi  9554  icoshftf1o  9927  maxabslemval  11150  xrmaxiflemval  11191  fisum0diag2  11388  alzdvds  11792  hashgcdeq  12171  tgcl  12704  distop  12725  neiuni  12801  cnpnei  12859  isxmetd  12987  fsumcncntop  13196  bj-nntrans2  13834  bj-inf2vnlem1  13852