Theorem ralrimivw 2435

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

Syntax hints:   -> wi 4   e. wcel 1433   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  exse  4091  sosng  4431  dmxpm  4573  exse2  4719  funco  4960  acexmidlemph  5525  mpt2eq12  5585  xpexgALT  5780  mpt2exg  5854  rdgtfr  5984  rdgruledefgg  5985  rdgivallem  5991  frecabex  6007  frectfr  6008  omfnex  6052  oeiv  6059  oeicl  6065  uniqs  6187  genpdisj  6713  ltexprlemloc  6797  recexprlemloc  6821  cauappcvgprlemrnd  6840  cauappcvgprlemdisj  6841  caucvgprlemrnd  6863  caucvgprlemdisj  6864  caucvgprprlemrnd  6891  caucvgprprlemdisj  6892  recan  9995  climconst  10129  dvdsext  10255