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