Theorem ssexnelpss

Description: If there is an element of a class which is not contained in a subclass, the subclass is a proper subclass. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Assertion	ssexnelpss	|- ( ( A C_ B /\ E. x e. B x e/ A ) -> A C. B )

Proof

Step	Hyp	Ref	Expression
1		df-nel	|- ( x e/ A <-> -. x e. A )
2		ssnelpss	|- ( A C_ B -> ( ( x e. B /\ -. x e. A ) -> A C. B ) )
3	2	expdimp	|- ( ( A C_ B /\ x e. B ) -> ( -. x e. A -> A C. B ) )
4	1 3	syl5bi	|- ( ( A C_ B /\ x e. B ) -> ( x e/ A -> A C. B ) )
5	4	rexlimdva	|- ( A C_ B -> ( E. x e. B x e/ A -> A C. B ) )
6	5	imp	|- ( ( A C_ B /\ E. x e. B x e/ A ) -> A C. B )