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	$$⊢\left(A\subseteq B\wedge \exists x\in Bx\notin A\right)\to A\subset B$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢x\notin A\leftrightarrow \neg x\in A$$
2		ssnelpss	$$⊢A\subseteq B\to \left(\left(x\in B\wedge \neg x\in A\right)\to A\subset B\right)$$
3	2	expdimp	$$⊢\left(A\subseteq B\wedge x\in B\right)\to \left(\neg x\in A\to A\subset B\right)$$
4	1 3	biimtrid	$$⊢\left(A\subseteq B\wedge x\in B\right)\to \left(x\notin A\to A\subset B\right)$$
5	4	rexlimdva	$$⊢A\subseteq B\to \left(\exists x\in Bx\notin A\to A\subset B\right)$$
6	5	imp	$$⊢\left(A\subseteq B\wedge \exists x\in Bx\notin A\right)\to A\subset B$$