Theorem rabssdv

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

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

Proof

Step	Hyp	Ref	Expression
1		rabssdv.1	$$⊢\left(\phi \wedge x\in A\wedge \psi \right)\to x\in B$$
2	1	3exp	$$⊢\phi \to \left(x\in A\to \left(\psi \to x\in B\right)\right)$$
3	2	ralrimiv	$$⊢\phi \to \forall x\in A\left(\psi \to x\in B\right)$$
4		rabss	$$⊢\left\{x\in A|\psi \right\}\subseteq B\leftrightarrow \forall x\in A\left(\psi \to x\in B\right)$$
5	3 4	sylibr	$$⊢\phi \to \left\{x\in A|\psi \right\}\subseteq B$$