Theorem ralrimiv 2578

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

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralrimiva  2579  ralrimivw  2580  ralrimivv  2587  r19.27av  2641  rr19.3v  2912  rabssdv  3273  rzal  3558  trin  4153  class2seteq  4208  ralxfrALT  4515  ssorduni  4536  ordsucim  4549  onintonm  4566  issref  5066  funimaexglem  5358  resflem  5746  poxp  6320  rdgss  6471  dom2lem  6865  supisoti  7114  ordiso2  7139  updjud  7186  uzind  9486  zindd  9493  lbzbi  9739  icoshftf1o  10115  ccatrn  11068  maxabslemval  11552  xrmaxiflemval  11594  fisum0diag2  11791  alzdvds  12198  hashgcdeq  12595  ghmrn  13626  ghmpreima  13635  imasring  13859  01eq0ring  13984  islssmd  14154  tgcl  14569  distop  14590  neiuni  14666  cnpnei  14724  isxmetd  14852  fsumcncntop  15072  fsumdvdsmul  15496  bj-nntrans2  15925  bj-inf2vnlem1  15943