Description: Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010) (Proof shortened by AV, 10-May-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nelelne | |- ( -. A e. B -> ( C e. B -> C =/= A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nelne2 | |- ( ( C e. B /\ -. A e. B ) -> C =/= A ) |
|
| 2 | 1 | expcom | |- ( -. A e. B -> ( C e. B -> C =/= A ) ) |