Metamath Proof Explorer

Theorem ssn0

Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007)

Ref Expression
Assertion ssn0 
|- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 sseq0 
 |-  ( ( A C_ B /\ B = (/) ) -> A = (/) )
2 1 ex 
 |-  ( A C_ B -> ( B = (/) -> A = (/) ) )
3 2 necon3d 
 |-  ( A C_ B -> ( A =/= (/) -> B =/= (/) ) )
4 3 imp 
 |-  ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )