Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012) (Proof shortened by Wolf Lammen, 14-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nelne2 | |- ( ( A e. C /\ -. B e. C ) -> A =/= B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nelneq | |- ( ( A e. C /\ -. B e. C ) -> -. A = B ) |
|
| 2 | 1 | neqned | |- ( ( A e. C /\ -. B e. C ) -> A =/= B ) |