Metamath Proof Explorer

Theorem ss2abi

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995)

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

Proof

Step Hyp Ref Expression
1 ss2abi.1 
 |-  ( ph -> ps )
2 ss2ab 
 |-  ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )
3 2 1 mpgbir 
 |-  { x | ph } C_ { x | ps }