Theorem ralrimiv 2580

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

Syntax hints:   -> wi 4   e. wcel 2178   A.wral 2486

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  ralrimiva  2581  ralrimivw  2582  ralrimivv  2589  r19.27av  2643  rr19.3v  2919  rabssdv  3281  rzal  3566  trin  4168  class2seteq  4223  ralxfrALT  4532  ssorduni  4553  ordsucim  4566  onintonm  4583  issref  5084  funimaexglem  5376  resflem  5767  poxp  6341  rdgss  6492  dom2lem  6886  supisoti  7138  ordiso2  7163  updjud  7210  uzind  9519  zindd  9526  lbzbi  9772  icoshftf1o  10148  ccatrn  11103  maxabslemval  11634  xrmaxiflemval  11676  fisum0diag2  11873  alzdvds  12280  hashgcdeq  12677  ghmrn  13708  ghmpreima  13717  imasring  13941  01eq0ring  14066  islssmd  14236  tgcl  14651  distop  14672  neiuni  14748  cnpnei  14806  isxmetd  14934  fsumcncntop  15154  fsumdvdsmul  15578  bj-nntrans2  16087  bj-inf2vnlem1  16105