Theorem ralrimivw 2387

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

Syntax hints:   -> wi 4   e. wcel 1390  A.wral 2300

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305

This theorem is referenced by:  exse  4058  sosng  4356  dmxpm  4498  exse2  4642  funco  4883  acexmidlemph  5448  mpt2eq12  5507  xpexgALT  5702  mpt2exg  5776  rdgtfr  5901  rdgruledefgg  5902  rdgivallem  5908  frecabex  5923  frectfr  5924  omfnex  5968  oeiv  5975  oeicl  5981  uniqs  6100  genpdisj  6506  ltexprlemloc  6581  recexprlemloc  6603  cauappcvgprlemrnd  6622  cauappcvgprlemdisj  6623  caucvgprlemrnd  6644  caucvgprlemdisj  6645