Metamath Proof Explorer


Theorem compne

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 V A A

Proof

Step Hyp Ref Expression
1 vn0 V
2 id V A = A V A = A
3 difeq1 V A = A V A A = A A
4 difabs V A A = V A
5 difid A A =
6 3 4 5 3eqtr3g V A = A V A =
7 2 6 eqtr3d V A = A A =
8 7 difeq2d V A = A V A = V
9 dif0 V = V
10 8 9 eqtrdi V A = A V A = V
11 10 6 eqtr3d V A = A V =
12 11 necon3i V V A A
13 1 12 ax-mp V A A