Theorem ralrimiv 2622

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

Syntax hints:   -> wi 4   e. wcel 2209   A.wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  ralrimiva  2623  ralrimivw  2624  ralrimivv  2631  r19.27av  2686  rr19.3v  2965  rabssdv  3328  rzal  3625  trin  4237  class2seteq  4298  ralxfrALT  4611  ssorduni  4632  ordsucim  4645  onintonm  4662  issref  5168  funimaexglem  5462  resflem  5866  poxp  6461  rdgss  6647  dom2lem  7051  supisoti  7343  ordiso2  7368  updjud  7415  uzind  9739  zindd  9746  lbzbi  9998  icoshftf1o  10375  ccatrn  11358  ccatalpha  11362  maxabslemval  11955  xrmaxiflemval  11997  fisum0diag2  12195  alzdvds  12602  hashgcdeq  12999  ghmrn  14040  ghmpreima  14049  imasring  14345  01eq0ring  14472  islssmd  14671  tgcl  15091  distop  15112  neiuni  15188  cnpnei  15246  isxmetd  15374  fsumcncntop  15594  fsumdvdsmul  16022  uspgr2wlkeq  16523  clwwlkccatlem  16558  bj-nntrans2  16895  bj-inf2vnlem1  16913