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 VAA

Proof

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