Theorem ralrimivw 2606

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  r19.27v  2660  r19.28v  2661  exse  4433  sosng  4799  dmxpm  4952  exse2  5110  funco  5366  acexmidlemph  6010  mpoeq12  6080  xpexgALT  6294  opabn1stprc  6357  mpoexg  6375  rdgtfr  6539  rdgruledefgg  6540  rdgivallem  6546  frecabex  6563  frectfr  6565  omfnex  6616  oeiv  6623  uniqs  6761  exmidpw2en  7103  exmidssfi  7130  sbthlemi5  7159  sbthlemi6  7160  updjud  7280  exmidfodomrlemim  7411  exmidaclem  7422  exmidapne  7478  cc4f  7487  genpdisj  7742  ltexprlemloc  7826  recexprlemloc  7850  cauappcvgprlemrnd  7869  cauappcvgprlemdisj  7870  caucvgprlemrnd  7892  caucvgprlemdisj  7893  caucvgprprlemrnd  7920  caucvgprprlemdisj  7921  suplocexpr  7944  zsupssdc  10497  nninfinf  10704  recan  11669  climconst  11850  sumeq2ad  11929  dvdsext  12415  pc11  12903  ptex  13346  prdsex  13351  prdsval  13355  prdsbaslemss  13356  prdsbas  13358  imasex  13387  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfnlemg  13396  imasaddvallemg  13397  quslem  13406  grpinvfng  13626  scaffng  14322  neif  14864  lmconst  14939  cndis  14964  plyval  15455  lgsquadlem2  15806  2sqlem10  15853  vtxdumgrfival  16148  uspgr2wlkeq2  16216  pw1dceq  16605