This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 vsnex ⊢ { 𝑦 } ∈ 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 ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) )