Theorem rabssdv

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		rabssdv.1	|- ( ( ph /\ x e. A /\ ps ) -> x e. B )
2	1	3exp	|- ( ph -> ( x e. A -> ( ps -> x e. B ) ) )
3	2	ralrimiv	|- ( ph -> A. x e. A ( ps -> x e. B ) )
4		rabss	|- ( { x e. A | ps } C_ B <-> A. x e. A ( ps -> x e. B ) )
5	3 4	sylibr	|- ( ph -> { x e. A | ps } C_ B )