Theorem ralrimiv 2602

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

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralrimiva  2603  ralrimivw  2604  ralrimivv  2611  r19.27av  2666  rr19.3v  2942  rabssdv  3304  rzal  3589  trin  4192  class2seteq  4247  ralxfrALT  4558  ssorduni  4579  ordsucim  4592  onintonm  4609  issref  5111  funimaexglem  5404  resflem  5799  poxp  6378  rdgss  6529  dom2lem  6923  supisoti  7177  ordiso2  7202  updjud  7249  uzind  9558  zindd  9565  lbzbi  9811  icoshftf1o  10187  ccatrn  11144  maxabslemval  11719  xrmaxiflemval  11761  fisum0diag2  11958  alzdvds  12365  hashgcdeq  12762  ghmrn  13794  ghmpreima  13803  imasring  14027  01eq0ring  14153  islssmd  14323  tgcl  14738  distop  14759  neiuni  14835  cnpnei  14893  isxmetd  15021  fsumcncntop  15241  fsumdvdsmul  15665  uspgr2wlkeq  16076  bj-nntrans2  16315  bj-inf2vnlem1  16333