Theorem ssrabdv

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

	Ref	Expression
Hypotheses	ssrabdv.1	$$⊢\phi \to B\subseteq A$$
	ssrabdv.2	$$⊢\left(\phi \wedge x\in B\right)\to \psi$$
Assertion	ssrabdv	$$⊢\phi \to B\subseteq \left\{x\in A|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssrabdv.1	$$⊢\phi \to B\subseteq A$$
2		ssrabdv.2	$$⊢\left(\phi \wedge x\in B\right)\to \psi$$
3	2	ralrimiva	$$⊢\phi \to \forall x\in B\psi$$
4		ssrab	$$⊢B\subseteq \left\{x\in A|\psi \right\}\leftrightarrow \left(B\subseteq A\wedge \forall x\in B\psi \right)$$
5	1 3 4	sylanbrc	$$⊢\phi \to B\subseteq \left\{x\in A|\psi \right\}$$