Theorem ssrd

Description: Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypotheses	ssrd.0	$$⊢Ⅎx\phi$$
	ssrd.1	$$⊢\underset{\_}{Ⅎ}xA$$
	ssrd.2	$$⊢\underset{\_}{Ⅎ}xB$$
	ssrd.3	$$⊢\phi \to \left(x\in A\to x\in B\right)$$
Assertion	ssrd	$$⊢\phi \to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		ssrd.0	$$⊢Ⅎx\phi$$
2		ssrd.1	$$⊢\underset{\_}{Ⅎ}xA$$
3		ssrd.2	$$⊢\underset{\_}{Ⅎ}xB$$
4		ssrd.3	$$⊢\phi \to \left(x\in A\to x\in B\right)$$
5	1 4	alrimi	$$⊢\phi \to \forall x\left(x\in A\to x\in B\right)$$
6	2 3	dfss2f	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
7	5 6	sylibr	$$⊢\phi \to A\subseteq B$$