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  6650  rdgruledefgg  6651  rdgivallem  6657  frecabex  6674  frectfr  6676  omfnex  6727  oeiv  6734  uniqs  6872  exmidpw2en  7225  exmidssfi  7252  sbthlemi5  7285  sbthlemi6  7286  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  10689  nninfinf  10900  recan  11897  climconst  12080  sumeq2ad  12159  dvdsext  12646  pc11  13138  ptex  13676  imasex  13684  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfnlemg  13693  imasaddvallemg  13694  quslem  13703  grpinvfng  13907  prdsex  14278  prdsval  14279  prdsbaslemss  14280  prdsbas  14282  scaffng  14754  neif  15384  lmconst  15459  cndis  15484  plyval  15975  lgsquadlem2  16419  2sqlem10  16466  vtxdumgrfival  16761  uspgr2wlkeq2  16829  pw1dceq  17257  exmidnotnotr  17258  exmidcon  17259  exmidpeirce  17260  wexmiddiffi  17266  wexmiddifxy  17268