Theorem ralrimiv 2559

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

Syntax hints:   -> wi 4   e. wcel 2158   A.wral 2465

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470

This theorem is referenced by:  ralrimiva  2560  ralrimivw  2561  ralrimivv  2568  r19.27av  2622  rr19.3v  2888  rabssdv  3247  rzal  3532  trin  4123  class2seteq  4175  ralxfrALT  4479  ssorduni  4498  ordsucim  4511  onintonm  4528  issref  5023  funimaexglem  5311  resflem  5693  poxp  6246  rdgss  6397  dom2lem  6785  supisoti  7022  ordiso2  7047  updjud  7094  uzind  9377  zindd  9384  lbzbi  9629  icoshftf1o  10004  maxabslemval  11230  xrmaxiflemval  11271  fisum0diag2  11468  alzdvds  11873  hashgcdeq  12252  imasring  13307  01eq0ring  13404  islssmd  13543  tgcl  13835  distop  13856  neiuni  13932  cnpnei  13990  isxmetd  14118  fsumcncntop  14327  bj-nntrans2  14975  bj-inf2vnlem1  14993