Theorem ralrimivw 2604

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

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  r19.27v  2658  r19.28v  2659  exse  4431  sosng  4797  dmxpm  4950  exse2  5108  funco  5364  acexmidlemph  6006  mpoeq12  6076  xpexgALT  6290  opabn1stprc  6353  mpoexg  6371  rdgtfr  6535  rdgruledefgg  6536  rdgivallem  6542  frecabex  6559  frectfr  6561  omfnex  6612  oeiv  6619  uniqs  6757  exmidpw2en  7097  sbthlemi5  7151  sbthlemi6  7152  updjud  7272  exmidfodomrlemim  7402  exmidaclem  7413  exmidapne  7469  cc4f  7478  genpdisj  7733  ltexprlemloc  7817  recexprlemloc  7841  cauappcvgprlemrnd  7860  cauappcvgprlemdisj  7861  caucvgprlemrnd  7883  caucvgprlemdisj  7884  caucvgprprlemrnd  7911  caucvgprprlemdisj  7912  suplocexpr  7935  zsupssdc  10488  nninfinf  10695  recan  11660  climconst  11841  sumeq2ad  11920  dvdsext  12406  pc11  12894  ptex  13337  prdsex  13342  prdsval  13346  prdsbaslemss  13347  prdsbas  13349  imasex  13378  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfnlemg  13387  imasaddvallemg  13388  quslem  13397  grpinvfng  13617  scaffng  14313  neif  14855  lmconst  14930  cndis  14955  plyval  15446  lgsquadlem2  15797  2sqlem10  15844  vtxdumgrfival  16104  uspgr2wlkeq2  16163  pw1dceq  16541