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 )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  r19.27v  2678  r19.28v  2679  exse  4483  sosng  4850  dmxpm  5004  exse2  5164  funco  5420  acexmidlemph  6081  mpoeq12  6151  xpexgALT  6370  opabn1stprc  6433  mpoexg  6451  rdgtfr  6649  rdgruledefgg  6650  rdgivallem  6656  frecabex  6673  frectfr  6675  omfnex  6726  oeiv  6733  uniqs  6871  exmidpw2en  7223  exmidssfi  7250  sbthlemi5  7283  sbthlemi6  7284  updjud  7428  exmidfodomrlemim  7559  exmidaclem  7570  exmidapne  7632  cc4f  7641  genpdisj  7896  ltexprlemloc  7980  recexprlemloc  8004  cauappcvgprlemrnd  8023  cauappcvgprlemdisj  8024  caucvgprlemrnd  8046  caucvgprlemdisj  8047  caucvgprprlemrnd  8074  caucvgprprlemdisj  8075  suplocexpr  8098  zsupssdc  10690  nninfinf  10901  recan  11898  climconst  12081  sumeq2ad  12160  dvdsext  12647  pc11  13139  ptex  13677  imasex  13685  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfnlemg  13694  imasaddvallemg  13695  quslem  13704  grpinvfng  13908  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdsbas  14283  scaffng  14755  neif  15367  lmconst  15442  cndis  15467  plyval  15958  lgsquadlem2  16402  2sqlem10  16449  vtxdumgrfival  16744  uspgr2wlkeq2  16812  pw1dceq  17240  exmidnotnotr  17241  exmidcon  17242  exmidpeirce  17243  wexmiddiffi  17249  wexmiddifxy  17251