Theorem ralrimiv 2569

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

Syntax hints:   -> wi 4   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralrimiva  2570  ralrimivw  2571  ralrimivv  2578  r19.27av  2632  rr19.3v  2903  rabssdv  3263  rzal  3548  trin  4141  class2seteq  4196  ralxfrALT  4502  ssorduni  4523  ordsucim  4536  onintonm  4553  issref  5052  funimaexglem  5341  resflem  5726  poxp  6290  rdgss  6441  dom2lem  6831  supisoti  7076  ordiso2  7101  updjud  7148  uzind  9437  zindd  9444  lbzbi  9690  icoshftf1o  10066  maxabslemval  11373  xrmaxiflemval  11415  fisum0diag2  11612  alzdvds  12019  hashgcdeq  12408  ghmrn  13387  ghmpreima  13396  imasring  13620  01eq0ring  13745  islssmd  13915  tgcl  14300  distop  14321  neiuni  14397  cnpnei  14455  isxmetd  14583  fsumcncntop  14803  fsumdvdsmul  15227  bj-nntrans2  15598  bj-inf2vnlem1  15616