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  4338  sosng  4701  dmxpm  4849  exse2  5004  funco  5258  acexmidlemph  5870  mpoeq12  5937  xpexgALT  6136  mpoexg  6214  rdgtfr  6377  rdgruledefgg  6378  rdgivallem  6384  frecabex  6401  frectfr  6403  omfnex  6452  oeiv  6459  uniqs  6595  sbthlemi5  6962  sbthlemi6  6963  updjud  7083  exmidfodomrlemim  7202  exmidaclem  7209  exmidapne  7261  cc4f  7270  genpdisj  7524  ltexprlemloc  7608  recexprlemloc  7632  cauappcvgprlemrnd  7651  cauappcvgprlemdisj  7652  caucvgprlemrnd  7674  caucvgprlemdisj  7675  caucvgprprlemrnd  7702  caucvgprprlemdisj  7703  suplocexpr  7726  recan  11120  climconst  11300  sumeq2ad  11379  dvdsext  11863  zsupssdc  11957  pc11  12332  ptex  12718  prdsex  12723  imasex  12731  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfnlemg  12740  imasaddvallemg  12741  quslem  12750  grpinvfng  12922  scaffng  13404  neif  13726  lmconst  13801  cndis  13826  2sqlem10  14557