Theorem ralrimivw 2564

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 2562	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2160   A.wral 2468

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  r19.27v  2617  r19.28v  2618  exse  4351  sosng  4714  dmxpm  4862  exse2  5017  funco  5272  acexmidlemph  5885  mpoeq12  5952  xpexgALT  6153  mpoexg  6231  rdgtfr  6394  rdgruledefgg  6395  rdgivallem  6401  frecabex  6418  frectfr  6420  omfnex  6469  oeiv  6476  uniqs  6614  exmidpw2en  6935  sbthlemi5  6985  sbthlemi6  6986  updjud  7106  exmidfodomrlemim  7225  exmidaclem  7232  exmidapne  7284  cc4f  7293  genpdisj  7547  ltexprlemloc  7631  recexprlemloc  7655  cauappcvgprlemrnd  7674  cauappcvgprlemdisj  7675  caucvgprlemrnd  7697  caucvgprlemdisj  7698  caucvgprprlemrnd  7725  caucvgprprlemdisj  7726  suplocexpr  7749  recan  11145  climconst  11325  sumeq2ad  11404  dvdsext  11888  zsupssdc  11982  pc11  12358  ptex  12762  prdsex  12767  imasex  12775  imasbas  12777  imasplusg  12778  imasmulr  12779  imasaddfnlemg  12784  imasaddvallemg  12785  quslem  12794  grpinvfng  12981  scaffng  13618  neif  14078  lmconst  14153  cndis  14178  2sqlem10  14909