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 
|- ( A =/= (/) -> E. x ( x C_ A /\ x =/= (/) ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( A =/= (/) <-> E. y y e. A )
2 vex 
 |-  y e. _V
3 2 snss 
 |-  ( y e. A <-> { y } C_ A )
4 2 snnz 
 |-  { y } =/= (/)
5 snex 
 |-  { y } e. _V
6 sseq1 
 |-  ( x = { y } -> ( x C_ A <-> { y } C_ A ) )
7 neeq1 
 |-  ( x = { y } -> ( x =/= (/) <-> { y } =/= (/) ) )
8 6 7 anbi12d 
 |-  ( x = { y } -> ( ( x C_ A /\ x =/= (/) ) <-> ( { y } C_ A /\ { y } =/= (/) ) ) )
9 5 8 spcev 
 |-  ( ( { y } C_ A /\ { y } =/= (/) ) -> E. x ( x C_ A /\ x =/= (/) ) )
10 4 9 mpan2 
 |-  ( { y } C_ A -> E. x ( x C_ A /\ x =/= (/) ) )
11 3 10 sylbi 
 |-  ( y e. A -> E. x ( x C_ A /\ x =/= (/) ) )
12 11 exlimiv 
 |-  ( E. y y e. A -> E. x ( x C_ A /\ x =/= (/) ) )
13 1 12 sylbi 
 |-  ( A =/= (/) -> E. x ( x C_ A /\ x =/= (/) ) )