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  6658  dom2lem  7062  supisoti  7356  ordiso2  7381  updjud  7428  uzind  9768  zindd  9775  lbzbi  10032  icoshftf1o  10410  ccatrn  11399  ccatalpha  11403  maxabslemval  11997  xrmaxiflemval  12041  fisum0diag2  12239  alzdvds  12646  hashgcdeq  13047  ghmrn  14119  ghmpreima  14128  cntz2ss  14168  imasring  14478  01eq0ring  14605  islssmd  14805  tgcl  15290  distop  15311  neiuni  15387  cnpnei  15445  isxmetd  15573  fsumcncntop  15793  fsumdvdsmul  16285  uspgr2wlkeq  16811  clwwlkccatlem  16846  bj-nntrans2  17183  bj-inf2vnlem1  17201