Theorem ralrimivw 2604

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
ralrimivw.1	|- ( ph -> ps )

Assertion

Ref	Expression
ralrimivw	|- ( ph -> A. x e. A ps )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem ralrimivw

Step	Hyp	Ref	Expression
1		ralrimivw.1	. . 3 |- ( ph -> ps )
2	1	a1d 22	. 2 |- ( ph -> ( x e. A -> ps ) )
3	2	ralrimiv 2602	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:  r19.27v  2658  r19.28v  2659  exse  4427  sosng  4792  dmxpm  4944  exse2  5102  funco  5358  acexmidlemph  5994  mpoeq12  6064  xpexgALT  6278  mpoexg  6357  rdgtfr  6520  rdgruledefgg  6521  rdgivallem  6527  frecabex  6544  frectfr  6546  omfnex  6595  oeiv  6602  uniqs  6740  exmidpw2en  7074  sbthlemi5  7128  sbthlemi6  7129  updjud  7249  exmidfodomrlemim  7379  exmidaclem  7390  exmidapne  7446  cc4f  7455  genpdisj  7710  ltexprlemloc  7794  recexprlemloc  7818  cauappcvgprlemrnd  7837  cauappcvgprlemdisj  7838  caucvgprlemrnd  7860  caucvgprlemdisj  7861  caucvgprprlemrnd  7888  caucvgprprlemdisj  7889  suplocexpr  7912  zsupssdc  10458  nninfinf  10665  recan  11620  climconst  11801  sumeq2ad  11880  dvdsext  12366  pc11  12854  ptex  13297  prdsex  13302  prdsval  13306  prdsbaslemss  13307  prdsbas  13309  imasex  13338  imasbas  13340  imasplusg  13341  imasmulr  13342  imasaddfnlemg  13347  imasaddvallemg  13348  quslem  13357  grpinvfng  13577  scaffng  14273  neif  14815  lmconst  14890  cndis  14915  plyval  15406  lgsquadlem2  15757  2sqlem10  15804  uspgr2wlkeq2  16077