Metamath Proof Explorer

Theorem nssne2

Description: Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015)

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

Proof

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