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  4481  sosng  4848  dmxpm  5002  exse2  5161  funco  5417  acexmidlemph  6078  mpoeq12  6148  xpexgALT  6366  opabn1stprc  6429  mpoexg  6447  rdgtfr  6645  rdgruledefgg  6646  rdgivallem  6652  frecabex  6669  frectfr  6671  omfnex  6722  oeiv  6729  uniqs  6867  exmidpw2en  7219  exmidssfi  7246  sbthlemi5  7278  sbthlemi6  7279  updjud  7422  exmidfodomrlemim  7553  exmidaclem  7564  exmidapne  7626  cc4f  7635  genpdisj  7890  ltexprlemloc  7974  recexprlemloc  7998  cauappcvgprlemrnd  8017  cauappcvgprlemdisj  8018  caucvgprlemrnd  8040  caucvgprlemdisj  8041  caucvgprprlemrnd  8068  caucvgprprlemdisj  8069  suplocexpr  8092  zsupssdc  10683  nninfinf  10893  recan  11890  climconst  12072  sumeq2ad  12151  dvdsext  12638  pc11  13130  ptex  13667  imasex  13675  imasbas  13677  imasplusg  13678  imasmulr  13679  imasaddfnlemg  13684  imasaddvallemg  13685  quslem  13694  grpinvfng  13898  prdsex  14221  prdsval  14222  prdsbaslemss  14223  prdsbas  14225  scaffng  14695  neif  15291  lmconst  15366  cndis  15391  plyval  15882  lgsquadlem2  16295  2sqlem10  16342  vtxdumgrfival  16637  uspgr2wlkeq2  16705  pw1dceq  17133  exmidnotnotr  17134  exmidcon  17135  exmidpeirce  17136  wexmiddiffi  17142  wexmiddifxy  17144