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 sseq0b 
 |-  ( B = (/) -> ( A C_ B <-> A = (/) ) )
2 1 biimpac 
 |-  ( ( A C_ B /\ B = (/) ) -> A = (/) )