Theorem ralrimivw 2607

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

Syntax hints:   -> wi 4   e. wcel 2202   A.wral 2511

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  r19.27v  2661  r19.28v  2662  exse  4439  sosng  4805  dmxpm  4958  exse2  5117  funco  5373  acexmidlemph  6021  mpoeq12  6091  xpexgALT  6304  opabn1stprc  6367  mpoexg  6385  rdgtfr  6583  rdgruledefgg  6584  rdgivallem  6590  frecabex  6607  frectfr  6609  omfnex  6660  oeiv  6667  uniqs  6805  exmidpw2en  7147  exmidssfi  7174  sbthlemi5  7203  sbthlemi6  7204  updjud  7341  exmidfodomrlemim  7472  exmidaclem  7483  exmidapne  7539  cc4f  7548  genpdisj  7803  ltexprlemloc  7887  recexprlemloc  7911  cauappcvgprlemrnd  7930  cauappcvgprlemdisj  7931  caucvgprlemrnd  7953  caucvgprlemdisj  7954  caucvgprprlemrnd  7981  caucvgprprlemdisj  7982  suplocexpr  8005  zsupssdc  10561  nninfinf  10768  recan  11749  climconst  11930  sumeq2ad  12009  dvdsext  12496  pc11  12984  ptex  13427  prdsex  13432  prdsval  13436  prdsbaslemss  13437  prdsbas  13439  imasex  13468  imasbas  13470  imasplusg  13471  imasmulr  13472  imasaddfnlemg  13477  imasaddvallemg  13478  quslem  13487  grpinvfng  13707  scaffng  14405  neif  14952  lmconst  15027  cndis  15052  plyval  15543  lgsquadlem2  15897  2sqlem10  15944  vtxdumgrfival  16239  uspgr2wlkeq2  16307  pw1dceq  16726  exmidnotnotr  16727  exmidcon  16728  exmidpeirce  16729