Description: The complement of A is not equal to A . (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by BJ, 11-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | compne | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vn0 | |
|
2 | id | |
|
3 | difeq1 | |
|
4 | difabs | |
|
5 | difid | |
|
6 | 3 4 5 | 3eqtr3g | |
7 | 2 6 | eqtr3d | |
8 | 7 | difeq2d | |
9 | dif0 | |
|
10 | 8 9 | eqtrdi | |
11 | 10 6 | eqtr3d | |
12 | 11 | necon3i | |
13 | 1 12 | ax-mp | |