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  4321  sosng  4684  dmxpm  4831  exse2  4985  funco  5238  acexmidlemph  5846  mpoeq12  5913  xpexgALT  6112  mpoexg  6190  rdgtfr  6353  rdgruledefgg  6354  rdgivallem  6360  frecabex  6377  frectfr  6379  omfnex  6428  oeiv  6435  uniqs  6571  sbthlemi5  6938  sbthlemi6  6939  updjud  7059  exmidfodomrlemim  7178  exmidaclem  7185  cc4f  7231  genpdisj  7485  ltexprlemloc  7569  recexprlemloc  7593  cauappcvgprlemrnd  7612  cauappcvgprlemdisj  7613  caucvgprlemrnd  7635  caucvgprlemdisj  7636  caucvgprprlemrnd  7663  caucvgprprlemdisj  7664  suplocexpr  7687  recan  11073  climconst  11253  sumeq2ad  11332  dvdsext  11815  zsupssdc  11909  pc11  12284  grpinvfng  12747  neif  12935  lmconst  13010  cndis  13035  2sqlem10  13755