Theorem ralrimivw 2582

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

Syntax hints:   -> wi 4   e. wcel 2178   A.wral 2486

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  r19.27v  2635  r19.28v  2636  exse  4401  sosng  4766  dmxpm  4917  exse2  5075  funco  5330  acexmidlemph  5960  mpoeq12  6028  xpexgALT  6241  mpoexg  6320  rdgtfr  6483  rdgruledefgg  6484  rdgivallem  6490  frecabex  6507  frectfr  6509  omfnex  6558  oeiv  6565  uniqs  6703  exmidpw2en  7035  sbthlemi5  7089  sbthlemi6  7090  updjud  7210  exmidfodomrlemim  7340  exmidaclem  7351  exmidapne  7407  cc4f  7416  genpdisj  7671  ltexprlemloc  7755  recexprlemloc  7779  cauappcvgprlemrnd  7798  cauappcvgprlemdisj  7799  caucvgprlemrnd  7821  caucvgprlemdisj  7822  caucvgprprlemrnd  7849  caucvgprprlemdisj  7850  suplocexpr  7873  zsupssdc  10418  nninfinf  10625  recan  11535  climconst  11716  sumeq2ad  11795  dvdsext  12281  pc11  12769  ptex  13211  prdsex  13216  prdsval  13220  prdsbaslemss  13221  prdsbas  13223  imasex  13252  imasbas  13254  imasplusg  13255  imasmulr  13256  imasaddfnlemg  13261  imasaddvallemg  13262  quslem  13271  grpinvfng  13491  scaffng  14186  neif  14728  lmconst  14803  cndis  14828  plyval  15319  lgsquadlem2  15670  2sqlem10  15717