Metamath Proof Explorer

Theorem ralrimivw

Description: Inference from Theorem 19.21 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014)

Ref Expression
Hypothesis ralrimivw.1 
|- ( ph -> ps )
Assertion ralrimivw 
|- ( ph -> A. x e. A ps )

Proof

Step Hyp Ref Expression
1 ralrimivw.1 
 |-  ( ph -> ps )
2 1 a1d 
 |-  ( ph -> ( x e. A -> ps ) )
3 2 ralrimiv 
 |-  ( ph -> A. x e. A ps )