Theorem ssrabdv

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006)

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

Proof

Step	Hyp	Ref	Expression
1		ssrabdv.1	|- ( ph -> B C_ A )
2		ssrabdv.2	|- ( ( ph /\ x e. B ) -> ps )
3	2	ralrimiva	|- ( ph -> A. x e. B ps )
4		ssrab	|- ( B C_ { x e. A | ps } <-> ( B C_ A /\ A. x e. B ps ) )
5	1 3 4	sylanbrc	|- ( ph -> B C_ { x e. A | ps } )