Theorem ssnelpssd

Description: Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ssnelpssd.1	$$⊢\phi \to A\subseteq B$$
	ssnelpssd.2	$$⊢\phi \to C\in B$$
	ssnelpssd.3	$$⊢\phi \to \neg C\in A$$
Assertion	ssnelpssd	$$⊢\phi \to A\subset B$$

Proof

Step	Hyp	Ref	Expression
1		ssnelpssd.1	$$⊢\phi \to A\subseteq B$$
2		ssnelpssd.2	$$⊢\phi \to C\in B$$
3		ssnelpssd.3	$$⊢\phi \to \neg C\in A$$
4		ssnelpss	$$⊢A\subseteq B\to \left(\left(C\in B\wedge \neg C\in A\right)\to A\subset B\right)$$
5	1 4	syl	$$⊢\phi \to \left(\left(C\in B\wedge \neg C\in A\right)\to A\subset B\right)$$
6	2 3 5	mp2and	$$⊢\phi \to A\subset B$$