Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012) (Proof shortened by Wolf Lammen, 14-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nelne1 | |- ( ( A e. B /\ -. A e. C ) -> B =/= C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nelneq2 | |- ( ( A e. B /\ -. A e. C ) -> -. B = C ) |
|
| 2 | 1 | neqned | |- ( ( A e. B /\ -. A e. C ) -> B =/= C ) |