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  3264  rzal  3549  trin  4142  class2seteq  4197  ralxfrALT  4503  ssorduni  4524  ordsucim  4537  onintonm  4554  issref  5053  funimaexglem  5342  resflem  5729  poxp  6299  rdgss  6450  dom2lem  6840  supisoti  7085  ordiso2  7110  updjud  7157  uzind  9454  zindd  9461  lbzbi  9707  icoshftf1o  10083  maxabslemval  11390  xrmaxiflemval  11432  fisum0diag2  11629  alzdvds  12036  hashgcdeq  12433  ghmrn  13463  ghmpreima  13472  imasring  13696  01eq0ring  13821  islssmd  13991  tgcl  14384  distop  14405  neiuni  14481  cnpnei  14539  isxmetd  14667  fsumcncntop  14887  fsumdvdsmul  15311  bj-nntrans2  15682  bj-inf2vnlem1  15700