Theorem ralrimivw 2539

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

Syntax hints:   -> wi 4   e. wcel 2136   A.wral 2443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448

This theorem is referenced by:  r19.27v  2592  r19.28v  2593  exse  4313  sosng  4676  dmxpm  4823  exse2  4977  funco  5227  acexmidlemph  5834  mpoeq12  5898  xpexgALT  6098  mpoexg  6176  rdgtfr  6338  rdgruledefgg  6339  rdgivallem  6345  frecabex  6362  frectfr  6364  omfnex  6413  oeiv  6420  uniqs  6555  sbthlemi5  6922  sbthlemi6  6923  updjud  7043  exmidfodomrlemim  7153  exmidaclem  7160  cc4f  7206  genpdisj  7460  ltexprlemloc  7544  recexprlemloc  7568  cauappcvgprlemrnd  7587  cauappcvgprlemdisj  7588  caucvgprlemrnd  7610  caucvgprlemdisj  7611  caucvgprprlemrnd  7638  caucvgprprlemdisj  7639  suplocexpr  7662  recan  11047  climconst  11227  sumeq2ad  11306  dvdsext  11789  zsupssdc  11883  pc11  12258  neif  12741  lmconst  12816  cndis  12841  2sqlem10  13561