Metamath Proof Explorer

Theorem elnelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020)

Ref Expression
Assertion elnelne2 
|- ( ( A e. C /\ B e/ C ) -> A =/= B )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( B e/ C <-> -. B e. C )
2 nelne2 
 |-  ( ( A e. C /\ -. B e. C ) -> A =/= B )
3 1 2 sylan2b 
 |-  ( ( A e. C /\ B e/ C ) -> A =/= B )