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	|- ( ph -> A C_ B )
	ssnelpssd.2	|- ( ph -> C e. B )
	ssnelpssd.3	|- ( ph -> -. C e. A )
Assertion	ssnelpssd	|- ( ph -> A C. B )

Proof

Step	Hyp	Ref	Expression
1		ssnelpssd.1	|- ( ph -> A C_ B )
2		ssnelpssd.2	|- ( ph -> C e. B )
3		ssnelpssd.3	|- ( ph -> -. C e. A )
4		ssnelpss	|- ( A C_ B -> ( ( C e. B /\ -. C e. A ) -> A C. B ) )
5	1 4	syl	|- ( ph -> ( ( C e. B /\ -. C e. A ) -> A C. B ) )
6	2 3 5	mp2and	|- ( ph -> A C. B )