Theorem ralrimivw 2624

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

Syntax hints:   -> wi 4   e. wcel 2209   A.wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  r19.27v  2678  r19.28v  2679  exse  4476  sosng  4843  dmxpm  4997  exse2  5156  funco  5412  acexmidlemph  6068  mpoeq12  6138  xpexgALT  6356  opabn1stprc  6419  mpoexg  6437  rdgtfr  6635  rdgruledefgg  6636  rdgivallem  6642  frecabex  6659  frectfr  6661  omfnex  6712  oeiv  6719  uniqs  6857  exmidpw2en  7209  exmidssfi  7236  sbthlemi5  7268  sbthlemi6  7269  updjud  7412  exmidfodomrlemim  7543  exmidaclem  7554  exmidapne  7616  cc4f  7625  genpdisj  7880  ltexprlemloc  7964  recexprlemloc  7988  cauappcvgprlemrnd  8007  cauappcvgprlemdisj  8008  caucvgprlemrnd  8030  caucvgprlemdisj  8031  caucvgprprlemrnd  8058  caucvgprprlemdisj  8059  suplocexpr  8082  zsupssdc  10651  nninfinf  10858  recan  11853  climconst  12034  sumeq2ad  12113  dvdsext  12600  pc11  13088  ptex  13595  imasex  13603  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfnlemg  13612  imasaddvallemg  13613  quslem  13622  grpinvfng  13826  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdsbas  14153  scaffng  14618  neif  15165  lmconst  15240  cndis  15265  plyval  15756  lgsquadlem2  16111  2sqlem10  16158  vtxdumgrfival  16453  uspgr2wlkeq2  16521  pw1dceq  16948  exmidnotnotr  16949  exmidcon  16950  exmidpeirce  16951