Theorem ralrimiv 2549

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralrimiva  2550  ralrimivw  2551  ralrimivv  2558  r19.27av  2612  rr19.3v  2877  rabssdv  3236  rzal  3521  trin  4112  class2seteq  4164  ralxfrALT  4468  ssorduni  4487  ordsucim  4500  onintonm  4517  issref  5012  funimaexglem  5300  resflem  5681  poxp  6233  rdgss  6384  dom2lem  6772  supisoti  7009  ordiso2  7034  updjud  7081  uzind  9364  zindd  9371  lbzbi  9616  icoshftf1o  9991  maxabslemval  11217  xrmaxiflemval  11258  fisum0diag2  11455  alzdvds  11860  hashgcdeq  12239  01eq0ring  13330  tgcl  13567  distop  13588  neiuni  13664  cnpnei  13722  isxmetd  13850  fsumcncntop  14059  bj-nntrans2  14707  bj-inf2vnlem1  14725