nnullss

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

		Ref	Expression
	Assertion	nnullss	$⊢ A \neq \emptyset \to \exists x (x \subseteq A \land x \neq \emptyset)$

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

Metamath Proof Explorer