Theorem ralrimivw 2544

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

Syntax hints:   -> wi 4   e. wcel 2141   A.wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  r19.27v  2597  r19.28v  2598  exse  4319  sosng  4682  dmxpm  4829  exse2  4983  funco  5236  acexmidlemph  5843  mpoeq12  5910  xpexgALT  6109  mpoexg  6187  rdgtfr  6350  rdgruledefgg  6351  rdgivallem  6357  frecabex  6374  frectfr  6376  omfnex  6425  oeiv  6432  uniqs  6567  sbthlemi5  6934  sbthlemi6  6935  updjud  7055  exmidfodomrlemim  7165  exmidaclem  7172  cc4f  7218  genpdisj  7472  ltexprlemloc  7556  recexprlemloc  7580  cauappcvgprlemrnd  7599  cauappcvgprlemdisj  7600  caucvgprlemrnd  7622  caucvgprlemdisj  7623  caucvgprprlemrnd  7650  caucvgprprlemdisj  7651  suplocexpr  7674  recan  11060  climconst  11240  sumeq2ad  11319  dvdsext  11802  zsupssdc  11896  pc11  12271  neif  12894  lmconst  12969  cndis  12994  2sqlem10  13714