Metamath Proof Explorer

Theorem nssne1

Description: Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015)

Ref Expression
Assertion nssne1 
|- ( ( A C_ B /\ -. A C_ C ) -> B =/= C )

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( B = C -> ( A C_ B <-> A C_ C ) )
2 1 biimpcd 
 |-  ( A C_ B -> ( B = C -> A C_ C ) )
3 2 necon3bd 
 |-  ( A C_ B -> ( -. A C_ C -> B =/= C ) )
4 3 imp 
 |-  ( ( A C_ B /\ -. A C_ C ) -> B =/= C )