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	syl6eq	$$⊢\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$$