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 }