Theorem ss2rabdv

Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006)

	Ref	Expression
Hypothesis	ss2rabdv.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
Assertion	ss2rabdv	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )

Proof

Step	Hyp	Ref	Expression
1		ss2rabdv.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ralrimiva	|- ( ph -> A. x e. A ( ps -> ch ) )
3		ss2rab	|- ( { x e. A | ps } C_ { x e. A | ch } <-> A. x e. A ( ps -> ch ) )
4	2 3	sylibr	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )