Metamath Proof Explorer

Theorem sseq0

Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( B = (/) -> ( A C_ B <-> A C_ (/) ) )
2 ss0 
 |-  ( A C_ (/) -> A = (/) )
3 1 2 biimtrdi 
 |-  ( B = (/) -> ( A C_ B -> A = (/) ) )
4 3 impcom 
 |-  ( ( A C_ B /\ B = (/) ) -> A = (/) )