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		vsnex	|- { 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 =/= (/) ) )