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  6000  mpoeq12  6070  xpexgALT  6284  mpoexg  6363  rdgtfr  6526  rdgruledefgg  6527  rdgivallem  6533  frecabex  6550  frectfr  6552  omfnex  6603  oeiv  6610  uniqs  6748  exmidpw2en  7085  sbthlemi5  7139  sbthlemi6  7140  updjud  7260  exmidfodomrlemim  7390  exmidaclem  7401  exmidapne  7457  cc4f  7466  genpdisj  7721  ltexprlemloc  7805  recexprlemloc  7829  cauappcvgprlemrnd  7848  cauappcvgprlemdisj  7849  caucvgprlemrnd  7871  caucvgprlemdisj  7872  caucvgprprlemrnd  7899  caucvgprprlemdisj  7900  suplocexpr  7923  zsupssdc  10470  nninfinf  10677  recan  11636  climconst  11817  sumeq2ad  11896  dvdsext  12382  pc11  12870  ptex  13313  prdsex  13318  prdsval  13322  prdsbaslemss  13323  prdsbas  13325  imasex  13354  imasbas  13356  imasplusg  13357  imasmulr  13358  imasaddfnlemg  13363  imasaddvallemg  13364  quslem  13373  grpinvfng  13593  scaffng  14289  neif  14831  lmconst  14906  cndis  14931  plyval  15422  lgsquadlem2  15773  2sqlem10  15820  vtxdumgrfival  16058  uspgr2wlkeq2  16112  pw1dceq  16457