Theorem ssnelpssd 3891

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

Hypotheses

Ref	Expression
ssnelpssd.1
ssnelpssd.2
ssnelpssd.3

Assertion

Ref	Expression
ssnelpssd

Proof of Theorem ssnelpssd

Step	Hyp	Ref	Expression
1		ssnelpssd.2	. 2
2		ssnelpssd.3	. 2
3		ssnelpssd.1	. . 3
4		ssnelpss 3890	. . 3
5	3, 4	syl 16	. 2
6	1, 2, 5	mp2and 679	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  e.wcel 1818  C_wss 3475  C.wpss 3476

This theorem is referenced by:  isfin4-3  8716  canth4  9046  mrieqv2d  15036  symggen  16495  pgpfac1lem1  17125  pgpfaclem2  17133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-ne 2654  df-pss 3491