Theorem ralrimiv 2616

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

Syntax hints:   -> wi 4   e. wcel 2205   A.wral 2522

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralrimiva  2617  ralrimivw  2618  ralrimivv  2625  r19.27av  2680  rr19.3v  2958  rabssdv  3320  rzal  3609  trin  4220  class2seteq  4278  ralxfrALT  4590  ssorduni  4611  ordsucim  4624  onintonm  4641  issref  5147  funimaexglem  5441  resflem  5843  poxp  6430  rdgss  6616  dom2lem  7013  supisoti  7303  ordiso2  7328  updjud  7375  uzind  9692  zindd  9699  lbzbi  9951  icoshftf1o  10327  ccatrn  11301  ccatalpha  11305  maxabslemval  11897  xrmaxiflemval  11939  fisum0diag2  12137  alzdvds  12544  hashgcdeq  12941  ghmrn  13991  ghmpreima  14000  imasring  14225  01eq0ring  14351  islssmd  14524  tgcl  14946  distop  14967  neiuni  15043  cnpnei  15101  isxmetd  15229  fsumcncntop  15449  fsumdvdsmul  15876  uspgr2wlkeq  16377  clwwlkccatlem  16412  bj-nntrans2  16739  bj-inf2vnlem1  16757