Metamath Proof Explorer

Theorem nelss

Description: Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015)

Ref Expression
Assertion nelss 
|- ( ( A e. B /\ -. A e. C ) -> -. B C_ C )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( B C_ C -> ( A e. B -> A e. C ) )
2 1 com12 
 |-  ( A e. B -> ( B C_ C -> A e. C ) )
3 2 con3dimp 
 |-  ( ( A e. B /\ -. A e. C ) -> -. B C_ C )