Theorem ralrimiv 2622

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralrimiva  2623  ralrimivw  2624  ralrimivv  2631  r19.27av  2686  rr19.3v  2965  rabssdv  3328  rzal  3625  trin  4239  class2seteq  4300  ralxfrALT  4613  ssorduni  4634  ordsucim  4647  onintonm  4664  issref  5170  funimaexglem  5464  resflem  5872  poxp  6468  rdgss  6654  dom2lem  7058  supisoti  7350  ordiso2  7375  updjud  7422  uzind  9761  zindd  9768  lbzbi  10025  icoshftf1o  10403  ccatrn  11391  ccatalpha  11395  maxabslemval  11989  xrmaxiflemval  12032  fisum0diag2  12230  alzdvds  12637  hashgcdeq  13038  ghmrn  14109  ghmpreima  14118  imasring  14418  01eq0ring  14545  islssmd  14745  tgcl  15214  distop  15235  neiuni  15311  cnpnei  15369  isxmetd  15497  fsumcncntop  15717  fsumdvdsmul  16186  uspgr2wlkeq  16704  clwwlkccatlem  16739  bj-nntrans2  17076  bj-inf2vnlem1  17094