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  2943  rabssdv  3305  rzal  3590  trin  4195  class2seteq  4251  ralxfrALT  4562  ssorduni  4583  ordsucim  4596  onintonm  4613  issref  5117  funimaexglem  5410  resflem  5807  poxp  6392  rdgss  6544  dom2lem  6940  supisoti  7200  ordiso2  7225  updjud  7272  uzind  9581  zindd  9588  lbzbi  9840  icoshftf1o  10216  ccatrn  11176  ccatalpha  11180  maxabslemval  11759  xrmaxiflemval  11801  fisum0diag2  11998  alzdvds  12405  hashgcdeq  12802  ghmrn  13834  ghmpreima  13843  imasring  14067  01eq0ring  14193  islssmd  14363  tgcl  14778  distop  14799  neiuni  14875  cnpnei  14933  isxmetd  15061  fsumcncntop  15281  fsumdvdsmul  15705  uspgr2wlkeq  16162  clwwlkccatlem  16195  bj-nntrans2  16483  bj-inf2vnlem1  16501