Theorem ralrimivw 2551

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  r19.27v  2604  r19.28v  2605  exse  4337  sosng  4700  dmxpm  4848  exse2  5003  funco  5257  acexmidlemph  5868  mpoeq12  5935  xpexgALT  6134  mpoexg  6212  rdgtfr  6375  rdgruledefgg  6376  rdgivallem  6382  frecabex  6399  frectfr  6401  omfnex  6450  oeiv  6457  uniqs  6593  sbthlemi5  6960  sbthlemi6  6961  updjud  7081  exmidfodomrlemim  7200  exmidaclem  7207  exmidapne  7259  cc4f  7268  genpdisj  7522  ltexprlemloc  7606  recexprlemloc  7630  cauappcvgprlemrnd  7649  cauappcvgprlemdisj  7650  caucvgprlemrnd  7672  caucvgprlemdisj  7673  caucvgprprlemrnd  7700  caucvgprprlemdisj  7701  suplocexpr  7724  recan  11118  climconst  11298  sumeq2ad  11377  dvdsext  11861  zsupssdc  11955  pc11  12330  ptex  12713  prdsex  12718  imasex  12726  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfnlemg  12735  imasaddvallemg  12736  quslem  12745  grpinvfng  12917  scaffng  13399  neif  13644  lmconst  13719  cndis  13744  2sqlem10  14475