Theorem ralrimivw 2568

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

Syntax hints:   -> wi 4   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  r19.27v  2621  r19.28v  2622  exse  4367  sosng  4732  dmxpm  4882  exse2  5039  funco  5294  acexmidlemph  5911  mpoeq12  5978  xpexgALT  6185  mpoexg  6264  rdgtfr  6427  rdgruledefgg  6428  rdgivallem  6434  frecabex  6451  frectfr  6453  omfnex  6502  oeiv  6509  uniqs  6647  exmidpw2en  6968  sbthlemi5  7020  sbthlemi6  7021  updjud  7141  exmidfodomrlemim  7261  exmidaclem  7268  exmidapne  7320  cc4f  7329  genpdisj  7583  ltexprlemloc  7667  recexprlemloc  7691  cauappcvgprlemrnd  7710  cauappcvgprlemdisj  7711  caucvgprlemrnd  7733  caucvgprlemdisj  7734  caucvgprprlemrnd  7761  caucvgprprlemdisj  7762  suplocexpr  7785  nninfinf  10514  recan  11253  climconst  11433  sumeq2ad  11512  dvdsext  11997  zsupssdc  12091  pc11  12469  ptex  12875  prdsex  12880  imasex  12888  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfnlemg  12897  imasaddvallemg  12898  quslem  12907  grpinvfng  13116  scaffng  13805  neif  14309  lmconst  14384  cndis  14409  plyval  14878  2sqlem10  15212