# 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 ${⊢}\mathrm{V}\setminus {A}\ne {A}$

### Proof

Step Hyp Ref Expression
1 vn0 ${⊢}\mathrm{V}\ne \varnothing$
2 id ${⊢}\mathrm{V}\setminus {A}={A}\to \mathrm{V}\setminus {A}={A}$
3 difeq1 ${⊢}\mathrm{V}\setminus {A}={A}\to \left(\mathrm{V}\setminus {A}\right)\setminus {A}={A}\setminus {A}$
4 difabs ${⊢}\left(\mathrm{V}\setminus {A}\right)\setminus {A}=\mathrm{V}\setminus {A}$
5 difid ${⊢}{A}\setminus {A}=\varnothing$
6 3 4 5 3eqtr3g ${⊢}\mathrm{V}\setminus {A}={A}\to \mathrm{V}\setminus {A}=\varnothing$
7 2 6 eqtr3d ${⊢}\mathrm{V}\setminus {A}={A}\to {A}=\varnothing$
8 7 difeq2d ${⊢}\mathrm{V}\setminus {A}={A}\to \mathrm{V}\setminus {A}=\mathrm{V}\setminus \varnothing$
9 dif0 ${⊢}\mathrm{V}\setminus \varnothing =\mathrm{V}$
10 8 9 eqtrdi ${⊢}\mathrm{V}\setminus {A}={A}\to \mathrm{V}\setminus {A}=\mathrm{V}$
11 10 6 eqtr3d ${⊢}\mathrm{V}\setminus {A}={A}\to \mathrm{V}=\varnothing$
12 11 necon3i ${⊢}\mathrm{V}\ne \varnothing \to \mathrm{V}\setminus {A}\ne {A}$
13 1 12 ax-mp ${⊢}\mathrm{V}\setminus {A}\ne {A}$