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  4241  class2seteq  4302  ralxfrALT  4615  ssorduni  4636  ordsucim  4649  onintonm  4666  issref  5173  funimaexglem  5467  resflem  5875  poxp  6472  rdgss  6659  dom2lem  7064  supisoti  7356  ordiso2  7381  updjud  7428  uzind  9767  zindd  9774  lbzbi  10031  icoshftf1o  10409  ccatrn  11398  ccatalpha  11402  maxabslemval  11996  xrmaxiflemval  12040  fisum0diag2  12238  alzdvds  12645  hashgcdeq  13046  ghmrn  14118  ghmpreima  14127  cntz2ss  14167  imasring  14477  01eq0ring  14604  islssmd  14804  tgcl  15307  distop  15328  neiuni  15404  cnpnei  15462  isxmetd  15590  fsumcncntop  15810  fsumdvdsmul  16302  uspgr2wlkeq  16828  clwwlkccatlem  16863  bj-nntrans2  17200  bj-inf2vnlem1  17218