Theorem ralrimiv 2549

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralrimiva  2550  ralrimivw  2551  ralrimivv  2558  r19.27av  2612  rr19.3v  2876  rabssdv  3235  rzal  3520  trin  4111  class2seteq  4163  ralxfrALT  4467  ssorduni  4486  ordsucim  4499  onintonm  4516  issref  5011  funimaexglem  5299  resflem  5680  poxp  6232  rdgss  6383  dom2lem  6771  supisoti  7008  ordiso2  7033  updjud  7080  uzind  9363  zindd  9370  lbzbi  9615  icoshftf1o  9990  maxabslemval  11216  xrmaxiflemval  11257  fisum0diag2  11454  alzdvds  11859  hashgcdeq  12238  01eq0ring  13328  tgcl  13534  distop  13555  neiuni  13631  cnpnei  13689  isxmetd  13817  fsumcncntop  14026  bj-nntrans2  14674  bj-inf2vnlem1  14692