Theorem nnullss

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

	Ref	Expression
Assertion	nnullss	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
2		vex	⊢ 𝑦 ∈ V
3	2	snss	⊢ ( 𝑦 ∈ 𝐴 ↔ { 𝑦 } ⊆ 𝐴 )
4	2	snnz	⊢ { 𝑦 } ≠ ∅
5		snex	⊢ { 𝑦 } ∈ V
6		sseq1	⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ⊆ 𝐴 ↔ { 𝑦 } ⊆ 𝐴 ) )
7		neeq1	⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ≠ ∅ ↔ { 𝑦 } ≠ ∅ ) )
8	6 7	anbi12d	⊢ ( 𝑥 = { 𝑦 } → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ↔ ( { 𝑦 } ⊆ 𝐴 ∧ { 𝑦 } ≠ ∅ ) ) )
9	5 8	spcev	⊢ ( ( { 𝑦 } ⊆ 𝐴 ∧ { 𝑦 } ≠ ∅ ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )
10	4 9	mpan2	⊢ ( { 𝑦 } ⊆ 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )
11	3 10	sylbi	⊢ ( 𝑦 ∈ 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )
12	11	exlimiv	⊢ ( ∃ 𝑦 𝑦 ∈ 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )
13	1 12	sylbi	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )