Metamath Proof Explorer


Theorem ss2rabi

Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999)

Ref Expression
Hypothesis ss2rabi.1
|- ( x e. A -> ( ph -> ps ) )
Assertion ss2rabi
|- { x e. A | ph } C_ { x e. A | ps }

Proof

Step Hyp Ref Expression
1 ss2rabi.1
 |-  ( x e. A -> ( ph -> ps ) )
2 ss2rab
 |-  ( { x e. A | ph } C_ { x e. A | ps } <-> A. x e. A ( ph -> ps ) )
3 2 1 mprgbir
 |-  { x e. A | ph } C_ { x e. A | ps }