Theorem ralrimivw 2509

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

Syntax hints:   -> wi 4   e. wcel 1481   A.wral 2417

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  r19.27v  2562  r19.28v  2563  exse  4266  sosng  4620  dmxpm  4767  exse2  4921  funco  5171  acexmidlemph  5775  mpoeq12  5839  xpexgALT  6039  mpoexg  6117  rdgtfr  6279  rdgruledefgg  6280  rdgivallem  6286  frecabex  6303  frectfr  6305  omfnex  6353  oeiv  6360  uniqs  6495  sbthlemi5  6857  sbthlemi6  6858  updjud  6975  exmidfodomrlemim  7074  exmidaclem  7081  cc4f  7101  genpdisj  7355  ltexprlemloc  7439  recexprlemloc  7463  cauappcvgprlemrnd  7482  cauappcvgprlemdisj  7483  caucvgprlemrnd  7505  caucvgprlemdisj  7506  caucvgprprlemrnd  7533  caucvgprprlemdisj  7534  suplocexpr  7557  recan  10913  climconst  11091  sumeq2ad  11170  dvdsext  11589  neif  12349  lmconst  12424  cndis  12449