Theorem nnullss

Description: A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003)

	Ref	Expression
Assertion	nnullss	$$⊢A\ne \varnothing \to \exists x\left(x\subseteq A\wedge x\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists yy\in A$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	snss	$$⊢y\in A\leftrightarrow \left\{y\right\}\subseteq A$$
4	2	snnz	$$⊢\left\{y\right\}\ne \varnothing$$
5		vsnex	$$⊢\left\{y\right\}\in \mathrm{V}$$
6		sseq1	$$⊢x=\left\{y\right\}\to \left(x\subseteq A\leftrightarrow \left\{y\right\}\subseteq A\right)$$
7		neeq1	$$⊢x=\left\{y\right\}\to \left(x\ne \varnothing \leftrightarrow \left\{y\right\}\ne \varnothing \right)$$
8	6 7	anbi12d	$$⊢x=\left\{y\right\}\to \left(\left(x\subseteq A\wedge x\ne \varnothing \right)\leftrightarrow \left(\left\{y\right\}\subseteq A\wedge \left\{y\right\}\ne \varnothing \right)\right)$$
9	5 8	spcev	$$⊢\left(\left\{y\right\}\subseteq A\wedge \left\{y\right\}\ne \varnothing \right)\to \exists x\left(x\subseteq A\wedge x\ne \varnothing \right)$$
10	4 9	mpan2	$$⊢\left\{y\right\}\subseteq A\to \exists x\left(x\subseteq A\wedge x\ne \varnothing \right)$$
11	3 10	sylbi	$$⊢y\in A\to \exists x\left(x\subseteq A\wedge x\ne \varnothing \right)$$
12	11	exlimiv	$$⊢\exists yy\in A\to \exists x\left(x\subseteq A\wedge x\ne \varnothing \right)$$
13	1 12	sylbi	$$⊢A\ne \varnothing \to \exists x\left(x\subseteq A\wedge x\ne \varnothing \right)$$