Theorem ralrimivw 2459

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

Syntax hints:   -> wi 4   e. wcel 1445   A.wral 2370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375

This theorem is referenced by:  exse  4187  sosng  4540  dmxpm  4687  exse2  4839  funco  5088  acexmidlemph  5683  mpt2eq12  5747  xpexgALT  5942  mpt2exg  6016  rdgtfr  6177  rdgruledefgg  6178  rdgivallem  6184  frecabex  6201  frectfr  6203  omfnex  6250  oeiv  6257  uniqs  6390  sbthlemi5  6750  sbthlemi6  6751  updjud  6853  exmidfodomrlemim  6924  genpdisj  7179  ltexprlemloc  7263  recexprlemloc  7287  cauappcvgprlemrnd  7306  cauappcvgprlemdisj  7307  caucvgprlemrnd  7329  caucvgprlemdisj  7330  caucvgprprlemrnd  7357  caucvgprprlemdisj  7358  recan  10657  climconst  10833  sumeq2ad  10912  dvdsext  11283  neif  11993  lmconst  12067  cndis  12092